Edit Profile Harper, Robert Compute Distance To: Compute Author ID: harper.robert Published as: Harper, Robert Homepage: http://www.cs.cmu.edu/~rwh/ External Links: MGP · Wikidata · ORCID · ResearchGate · dblp Member of Collective: the-univalent-foundations-program. Documents Indexed: 57 Publications since 1987, including 2 Books all top 5 Co-Authors 8 single-authored 8 Blelloch, Guy E. 8 Crary, Karl 6 Licata, Daniel R. 5 Pfenning, Frank 4 Angiuli, Carlo 2 Acar, Umut A. 2 Birkedal, Lars 2 Dreyer, Derek R. 2 Gibbons, Phillip B. 2 Lillibridge, Mark 2 Morehouse, Edward 2 Morrisett, Greg 2 Murphy, Tom VII 2 Nanevski, Aleksandar 2 Sannella, Donald T. 2 Spoonhower, Daniel 2 Stone, Christopher A. 2 Tarlecki, Andrzej 2 Tassarotti, Joseph 1 Benton, Nick 1 Biagioni, Edoardo 1 Burch, Hal 1 Chakravarty, Manuel M. T. 1 Chang, Bor-Yuh Evan 1 Colby, Christopher 1 DeLap, Margaret 1 Gordon, Andrew D. 1 Halpern, Joseph Yehuda 1 Harrison, John W. 1 Honsell, Furio 1 Hou (Favonia), Kuen-Bang 1 Immerman, Neil 1 Jeffrey, Alan S. A. 1 Jung, Ralf 1 Keller, Gabriele Cornelia 1 Kolaitis, Phokion G. 1 Kumar, Ananya 1 Lee, Daniel K. 1 Lee, Peter L. 1 Lee, Peter N. 1 Liszka, Jason 1 Mandelbaum, Yitzhak 1 Miller, Gary Lee 1 Milner, Robin 1 Mitchell, John C. 1 Petersen, Leaf 1 Plotkin, Gordon D. 1 Pollack, Robert 1 Sewell, Peter 1 Sterling, Jonathan 1 Tofte, Mads 1 Vardi, Moshe Y. 1 Vianu, Victor 1 Vittes, Jorge L. 1 Walker, David A. 1 Walkington, Noel J. 1 Wilson, Todd 1 Woo, Shan Leung Maverick 1 Xi, Hongwei all top 5 Serials 7 Journal of Functional Programming 3 Information Processing Letters 3 Theoretical Computer Science 3 Higher-Order and Symbolic Computation 2 ACM Transactions on Computational Logic 1 Journal of the Association for Computing Machinery 1 Annals of Pure and Applied Logic 1 Journal of Symbolic Computation 1 Information and Computation 1 Journal of Logic and Computation 1 Indagationes Mathematicae. New Series 1 The Bulletin of Symbolic Logic 1 Lecture Notes in Computer Science all top 5 Fields 54 Computer science (68-XX) 23 Mathematical logic and foundations (03-XX) 4 Algebraic topology (55-XX) 1 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) 1 Category theory; homological algebra (18-XX) 1 Numerical analysis (65-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH 43 Publications have been cited 377 times in 312 Documents Cited by ▼ Year ▼ A framework for defining logics. Zbl 0778.03004Harper, Robert; Honsell, Furio; Plotkin, Gordon 183 1993 Towards a mechanized metatheory of Standard ML. Zbl 1295.68088Lee, Daniel K.; Crary, Karl; Harper, Robert 16 2007 Structured theory presentations and logic representations. Zbl 0809.03019Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 15 1994 On equivalence and canonical forms in the LF type theory. Zbl 1367.03055Harper, Robert; Pfenning, Frank 13 2005 Mechanizing metatheory in a logical framework. Zbl 1125.68029Harper, Robert; Licata, Daniel R. 12 2007 Practical foundations for programming languages. 2nd edition. Zbl 1347.68001Harper, Robert 9 2016 Syntactic logical relations for polymorphic and recursive types. Zbl 1277.68119Crary, Karl; Harper, Robert 9 2007 A type system for higher-order modules. Zbl 1321.68167Dreyer, Derek; Crary, Karl; Harper, Robert 7 2003 Deciding type equivalence in a language with singleton kinds. Zbl 1323.68163Stone, Christopher A.; Harper, Robert 7 2000 Structure and representation in LF. Zbl 0716.68078Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 7 1989 Computational higher-dimensional type theory. Zbl 1380.68112Angiuli, Carlo; Harper, Robert; Wilson, Todd 6 2017 Extensional equivalence and singleton types. Zbl 1367.68055Stone, Christopher A.; Harper, Robert 6 2006 Distributed control flow with classical modal logic. Zbl 1136.68443Murphy, Tom VII; Crary, Karl; Harper, Robert 6 2005 Corrigendum: Polymorphic type assignment and CPS conversion. Zbl 1058.68727Harper, Robert; Lillibridge, Mark 6 2003 On the unusual effectiveness of logic in computer science. Zbl 0979.03033Halpern, Joseph Y.; Harper, Robert; Immerman, Neil; Kolaitis, Phokion G.; Vardi, Moshe Y.; Vianu, Victor 6 2001 Type checking with universes. Zbl 0737.68013Harper, Robert; Pollack, Robert 6 1991 A universe of binding and computation. Zbl 1302.68050Licata, Daniel R.; Harper, Robert 5 2009 Relational interpretations of recursive types in an operational setting. Zbl 1045.68504Birkedal, Lars; Harper, Robert 5 1999 A simplified account of polymorphic references. Zbl 0813.68131Harper, Robert 5 1994 Dynamizing static algorithms, with applications to dynamic trees and history independence. Zbl 1318.68080Acar, Umut A.; Blelloch, Guy E.; Harper, Robert; Vittes, Jorge L.; Woo, Shan Leung Maverick 4 2004 Parametricity and variants of Girard’s \(J\) operator. Zbl 1002.68024Harper, Robert; Mitchell, John C. 4 1999 Proof-directed debugging. Zbl 0948.68038Harper, Robert 4 1999 An effective theory of type refinements. Zbl 1315.68055Mandelbaum, Yitzhak; Walker, David; Harper, Robert 3 2003 Adaptive functional programming. Zbl 1322.68034Acar, Umut A.; Blelloch, Guy E.; Harper, Robert 3 2002 A dependently typed assembly language. Zbl 1323.68084Xi, Hongwei; Harper, Robert 3 2001 A module system for a programming language based on the LF logical framework. Zbl 0902.68031Harper, Robert; Pfenning, Frank 3 1998 Relational interpretations of recursive types in an operational setting. Zbl 0888.03016Birkedal, Lars; Harper, Robert 3 1997 2-dimensional directed type theory. Zbl 1343.03051Licata, Daniel R.; Harper, Robert 2 2011 Modular type classes. Zbl 1295.68061Dreyer, Derek; Harper, Robert; Chakravarty, Manuel M. T.; Keller, Gabriele 2 2007 Automatic generation of staged geometric predicates. Zbl 1323.68540Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert 2 2001 A note on “A simplified account of polymorphic references”. Zbl 0998.68534Harper, Robert 2 1996 A type discipline for program modules. Zbl 0614.68010Harper, Robert; Milner, Robin; Tofte, Mads 2 1987 Verified tail bounds for randomized programs. Zbl 06947002Tassarotti, Joseph; Harper, Robert 1 2018 Meaning explanations at higher dimension. Zbl 1436.03102Angiuli, Carlo; Harper, Robert 1 2018 A higher-order logic for concurrent termination-preserving refinement. Zbl 06721348Tassarotti, Joseph; Jung, Ralf; Harper, Robert 1 2017 Homotopical patch theory. Zbl 1345.68093Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert 1 2014 Canonicity for 2-dimensional type theory. Zbl 1321.03049Licata, Daniel R.; Harper, Robert 1 2012 A type theory for memory allocation and data layout. Zbl 1321.68181Petersen, Leaf; Harper, Robert; Crary, Karl; Pfenning, Frank 1 2003 Automatic generation of staged geometric predicates. Zbl 1059.68147Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert 1 2003 A network protocol stack in standard ML. Zbl 1017.68005Biagioni, Edoardo; Harper, Robert; Lee, Peter 1 2001 Typed closure conversion for recursively-defined functions. (Extended abstract). Zbl 0925.68298Morrisett, Greg; Harper, Robert 1 1997 Operational interpretations of an extension of \(F_ \omega\) with control operators. Zbl 0861.68055Harper, Robert; Lillibridge, Mark 1 1996 Constructing type systems over an operational semantics. Zbl 0766.68088Harper, Robert 1 1992 Verified tail bounds for randomized programs. Zbl 06947002Tassarotti, Joseph; Harper, Robert 1 2018 Meaning explanations at higher dimension. Zbl 1436.03102Angiuli, Carlo; Harper, Robert 1 2018 Computational higher-dimensional type theory. Zbl 1380.68112Angiuli, Carlo; Harper, Robert; Wilson, Todd 6 2017 A higher-order logic for concurrent termination-preserving refinement. Zbl 06721348Tassarotti, Joseph; Jung, Ralf; Harper, Robert 1 2017 Practical foundations for programming languages. 2nd edition. Zbl 1347.68001Harper, Robert 9 2016 Homotopical patch theory. Zbl 1345.68093Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert 1 2014 Canonicity for 2-dimensional type theory. Zbl 1321.03049Licata, Daniel R.; Harper, Robert 1 2012 2-dimensional directed type theory. Zbl 1343.03051Licata, Daniel R.; Harper, Robert 2 2011 A universe of binding and computation. Zbl 1302.68050Licata, Daniel R.; Harper, Robert 5 2009 Towards a mechanized metatheory of Standard ML. Zbl 1295.68088Lee, Daniel K.; Crary, Karl; Harper, Robert 16 2007 Mechanizing metatheory in a logical framework. Zbl 1125.68029Harper, Robert; Licata, Daniel R. 12 2007 Syntactic logical relations for polymorphic and recursive types. Zbl 1277.68119Crary, Karl; Harper, Robert 9 2007 Modular type classes. Zbl 1295.68061Dreyer, Derek; Harper, Robert; Chakravarty, Manuel M. T.; Keller, Gabriele 2 2007 Extensional equivalence and singleton types. Zbl 1367.68055Stone, Christopher A.; Harper, Robert 6 2006 On equivalence and canonical forms in the LF type theory. Zbl 1367.03055Harper, Robert; Pfenning, Frank 13 2005 Distributed control flow with classical modal logic. Zbl 1136.68443Murphy, Tom VII; Crary, Karl; Harper, Robert 6 2005 Dynamizing static algorithms, with applications to dynamic trees and history independence. Zbl 1318.68080Acar, Umut A.; Blelloch, Guy E.; Harper, Robert; Vittes, Jorge L.; Woo, Shan Leung Maverick 4 2004 A type system for higher-order modules. Zbl 1321.68167Dreyer, Derek; Crary, Karl; Harper, Robert 7 2003 Corrigendum: Polymorphic type assignment and CPS conversion. Zbl 1058.68727Harper, Robert; Lillibridge, Mark 6 2003 An effective theory of type refinements. Zbl 1315.68055Mandelbaum, Yitzhak; Walker, David; Harper, Robert 3 2003 A type theory for memory allocation and data layout. Zbl 1321.68181Petersen, Leaf; Harper, Robert; Crary, Karl; Pfenning, Frank 1 2003 Automatic generation of staged geometric predicates. Zbl 1059.68147Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert 1 2003 Adaptive functional programming. Zbl 1322.68034Acar, Umut A.; Blelloch, Guy E.; Harper, Robert 3 2002 On the unusual effectiveness of logic in computer science. Zbl 0979.03033Halpern, Joseph Y.; Harper, Robert; Immerman, Neil; Kolaitis, Phokion G.; Vardi, Moshe Y.; Vianu, Victor 6 2001 A dependently typed assembly language. Zbl 1323.68084Xi, Hongwei; Harper, Robert 3 2001 Automatic generation of staged geometric predicates. Zbl 1323.68540Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert 2 2001 A network protocol stack in standard ML. Zbl 1017.68005Biagioni, Edoardo; Harper, Robert; Lee, Peter 1 2001 Deciding type equivalence in a language with singleton kinds. Zbl 1323.68163Stone, Christopher A.; Harper, Robert 7 2000 Relational interpretations of recursive types in an operational setting. Zbl 1045.68504Birkedal, Lars; Harper, Robert 5 1999 Parametricity and variants of Girard’s \(J\) operator. Zbl 1002.68024Harper, Robert; Mitchell, John C. 4 1999 Proof-directed debugging. Zbl 0948.68038Harper, Robert 4 1999 A module system for a programming language based on the LF logical framework. Zbl 0902.68031Harper, Robert; Pfenning, Frank 3 1998 Relational interpretations of recursive types in an operational setting. Zbl 0888.03016Birkedal, Lars; Harper, Robert 3 1997 Typed closure conversion for recursively-defined functions. (Extended abstract). Zbl 0925.68298Morrisett, Greg; Harper, Robert 1 1997 A note on “A simplified account of polymorphic references”. Zbl 0998.68534Harper, Robert 2 1996 Operational interpretations of an extension of \(F_ \omega\) with control operators. Zbl 0861.68055Harper, Robert; Lillibridge, Mark 1 1996 Structured theory presentations and logic representations. Zbl 0809.03019Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 15 1994 A simplified account of polymorphic references. Zbl 0813.68131Harper, Robert 5 1994 A framework for defining logics. Zbl 0778.03004Harper, Robert; Honsell, Furio; Plotkin, Gordon 183 1993 Constructing type systems over an operational semantics. Zbl 0766.68088Harper, Robert 1 1992 Type checking with universes. Zbl 0737.68013Harper, Robert; Pollack, Robert 6 1991 Structure and representation in LF. Zbl 0716.68078Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 7 1989 A type discipline for program modules. Zbl 0614.68010Harper, Robert; Milner, Robin; Tofte, Mads 2 1987 all cited Publications top 5 cited Publications all top 5 Cited by 387 Authors 18 Rabe, Florian 14 Pientka, Brigitte 13 Harper, Robert 9 Honsell, Furio 9 Miller, Dale Allen 8 Felty, Amy P. 8 Kohlhase, Michael 7 Abel, Andreas M. 7 Horozal, Fulya 7 Miculan, Marino 7 Momigliano, Alberto 7 Pfenning, Frank 7 Tarlecki, Andrzej 6 Nadathur, Gopalan 6 Roşu, Grigore 6 Scagnetto, Ivan 5 Liquori, Luigi 5 Luo, Zhaohui 5 Meseguer Guaita, José 5 Rossberg, Andreas 5 Sannella, Donald T. 4 Cheney, James 4 Diaconescu, Răzvan 4 Geuvers, Jan Herman 4 Lenisa, Marina 4 Mossakowski, Till 4 Schürmann, Carsten 3 Angiuli, Carlo 3 Avron, Arnon 3 Barthe, Gilles 3 Birkedal, Lars 3 Cervesato, Iliano 3 Ciaffaglione, Alberto 3 Coquand, Thierry 3 Crary, Karl 3 Dreyer, Derek R. 3 Duggan, Dominic 3 Gacek, Andrew 3 Hatcliff, John 3 Iancu, Mihnea 3 Licata, Daniel R. 3 Nederpelt, Rob 3 Paulson, Lawrence Charles 3 Pitts, Andrew M. 3 Popescu, Andrei 3 Sørensen, Morten Heine B. 3 Stump, Aaron 3 Thiemann, Peter J. 3 Toninho, Bernardo 3 Yoshida, Nobuko 2 Acar, Umut A. 2 Adams, Robin 2 Anderson, Penny 2 Basin, David A. 2 Benton, Nick 2 Bonelli, Eduardo 2 Buchholtz, Ulrik 2 Cave, Andrew 2 Chihani, Zakaria 2 Codescu, Mihai 2 Crole, Roy L. 2 Despeyroux, Joëlle 2 Dunfield, Joshua 2 Feller, Federico 2 Galmiche, Didier 2 Hagiya, Masami 2 Hou (Favonia), Kuen-Bang 2 Kaliszyk, Cezary 2 Kamareddine, Fairouz D. 2 Mason, Ian A. 2 Matthews, Seán 2 Morehouse, Edward 2 Morrisett, Greg 2 Nanevski, Aleksandar 2 Nipkow, Tobias 2 Perera, Roly 2 Pion, Sylvain 2 Pollack, Randy 2 Pollack, Robert 2 Pottier, François 2 Pym, David J. 2 Reed, Jason 2 Russo, Claudio V. 2 Sacerdoti Coen, Claudio 2 Sato, Masahiko 2 Şerbănuţă, Traian Florin 2 Shan, Chung-chieh 2 Sheard, Tim 2 Sojakova, Kristina 2 Støvring, Kristian 2 Talcott, Carolyn L. 2 Thamsborg, Jacob 2 Urban, Christian 2 Uustalu, Tarmo 2 Vytiniotis, Dimitrios 2 Weber, Matthias 2 Weirich, Stephanie 2 Ziliani, Beta 1 Akama, Yohji 1 Albert, Elvira ...and 287 more Authors all top 5 Cited in 48 Serials 37 Theoretical Computer Science 28 Journal of Automated Reasoning 22 Journal of Functional Programming 20 Information and Computation 16 MSCS. Mathematical Structures in Computer Science 9 Formal Aspects of Computing 6 Annals of Pure and Applied Logic 5 Higher-Order and Symbolic Computation 5 Theory and Practice of Logic Programming 5 Logical Methods in Computer Science 4 Information Processing Letters 4 Journal of Computer Science and Technology 4 The Journal of Logic and Algebraic Programming 3 RAIRO. Theoretical Informatics and Applications 3 Journal of Applied Logic 2 Acta Informatica 2 Science of Computer Programming 2 Journal of Symbolic Computation 2 Discrete & Computational Geometry 2 Indagationes Mathematicae. New Series 2 The Bulletin of Symbolic Logic 2 ACM Transactions on Computational Logic 2 Logica Universalis 2 Journal of Logical and Algebraic Methods in Programming 1 The Mathematical Intelligencer 1 ACM Transactions on Mathematical Software 1 BIT 1 Cahiers de Topologie et Géométrie Différentielle Catégoriques 1 The Journal of Symbolic Logic 1 Programming and Computer Software 1 Studia Logica 1 Synthese 1 New Generation Computing 1 JETAI. Journal of Experimental & Theoretical Artificial Intelligence 1 International Journal of Foundations of Computer Science 1 Bulletin of the American Mathematical Society. New Series 1 Formal Methods in System Design 1 Journal of Logic, Language and Information 1 Applied Categorical Structures 1 Journal of Applied Non-Classical Logics 1 Journal of the ACM 1 Sādhanā 1 Electronic Notes in Theoretical Computer Science 1 The Review of Symbolic Logic 1 Journal of Formalized Reasoning 1 Frontiers of Computer Science in China 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Higher Structures all top 5 Cited in 13 Fields 275 Computer science (68-XX) 143 Mathematical logic and foundations (03-XX) 10 Category theory; homological algebra (18-XX) 5 Algebraic topology (55-XX) 3 History and biography (01-XX) 2 Numerical analysis (65-XX) 1 General and overarching topics; collections (00-XX) 1 Combinatorics (05-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 General algebraic systems (08-XX) 1 Manifolds and cell complexes (57-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.