Edit Profile (opens in new tab) Harper, Robert Co-Author Distance Author ID: harper.robert Published as: Harper, Robert Further Spellings: Harper, Robert William jr.; Harper, Bob Homepage: http://www.cs.cmu.edu/~rwh/ External Links: MGP · ORCID · Wikidata · ResearchGate · dblp · GND · IdRef Documents Indexed: 61 Publications since 1987, including 1 Book 2 Contributions as Editor · 1 Further Contribution Biographic References: 1 Publication Co-Authors: 58 Co-Authors with 56 Joint Publications 1,271 Co-Co-Authors all top 5 Co-Authors 8 single-authored 8 Blelloch, Guy E. 8 Crary, Karl 7 Angiuli, Carlo 7 Licata, Daniel R. 5 Pfenning, Frank 4 Hou (Favonia), Kuen-Bang 3 Sannella, Donald T. 3 Tarlecki, Andrzej 2 Acar, Umut A. 2 Birkedal, Lars 2 Brunerie, Guillaume 2 Cavallo, Evan 2 Coquand, Thierry 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 Spoonhower, Daniel 2 Sterling, Jonathan 2 Stone, Christopher A. 2 Tassarotti, Joseph 1 Aczel, Peter 1 Ahrens, Benedikt 1 Altenkirch, Thorsten 1 Avigad, Jeremy 1 Awodey, Steve 1 Barras, Bruno 1 Bauer, Andrej 1 Benton, Nick 1 Bertot, Yves 1 Bezem, Marc 1 Biagioni, Edoardo 1 Bordg, Anthony 1 Burch, Hal 1 Chakravarty, Manuel M. T. 1 Chang, Bor-Yuh Evan 1 Cohen, Cyril 1 Colby, Christopher 1 Constable, Robert Lee 1 Curien, Pierre-Louis 1 DeLap, Margaret 1 Dybjer, Peter 1 Finster, Eric 1 Gambino, Nicola 1 Garner, Richard 1 Gonthier, Georges 1 Gordon, Andrew D. 1 Grayson, Daniel Richard 1 Hales, Thomas Callister 1 Halpern, Joseph Yehuda 1 Herbelin, Hugo 1 Hofmann, Martin 1 Hofstra, Pieter J. W. 1 Honsell, Furio 1 Hötzel Escardó, Martín 1 Immerman, Neil 1 Jeffrey, Alan S. A. 1 Joyal, André 1 Jung, Ralf 1 Kapulkin, Krzysztof 1 Keller, Gabriele Cornelia 1 Kock, Joachim 1 Kolaitis, Phokion G. 1 Kraus, Nicolai 1 Kumar, Ananya 1 Lee, Daniel K. 1 Li, Nuo 1 Licata, Dan 1 Liszka, Jason 1 Lumsdaine, Peter LeFanu 1 Luo, Zhaohui 1 Mahboubi, Assia 1 Mandelbaum, Yitzhak 1 Martin-Löf, Per 1 Melikhov, Sergey Aleksandrovich 1 Miller, Gary Lee 1 Milner, Robin 1 Mitchell, John C. 1 Nahas, Michael 1 Palmgren, Erik 1 Pelayo, Alvaro 1 Petersen, Leaf 1 Plotkin, Gordon D. 1 Pollack, Robert 1 Polonsky, Andrew 1 Riehl, Emily 1 Rijke, Egbert 1 Scott, Dana Stewart 1 Scott, Philip J. 1 Sewell, Peter 1 Shulman, Michael A. 1 Sojakova, Kristina 1 Solov’ëv, Sergeĭ Vladimirovich 1 Sozeau, Matthieu 1 Spitters, Bas 1 1 Tofte, Mads ...and 11 more Co-Authors 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 MSCS. Mathematical Structures in Computer Science 1 Indagationes Mathematicae. New Series 1 The Bulletin of Symbolic Logic 1 Journal of the ACM 1 Lecture Notes in Computer Science 1 Logical Methods in Computer Science all top 5 Fields 57 Computer science (68-XX) 31 Mathematical logic and foundations (03-XX) 5 Algebraic topology (55-XX) 3 Category theory; homological algebra (18-XX) 1 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) 1 Numerical analysis (65-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 50 Publications have been cited 495 times in 390 Documents Cited by ▼ Year ▼ A framework for defining logics. Zbl 0778.03004Harper, Robert; Honsell, Furio; Plotkin, Gordon 212 1993 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 128 2013 Practical foundations for programming languages. 2nd edition. Zbl 1347.68001Harper, Robert 21 2016 Towards a mechanized metatheory of Standard ML. Zbl 1295.68088Lee, Daniel K.; Crary, Karl; Harper, Robert 20 2007 On equivalence and canonical forms in the LF type theory. Zbl 1367.03055Harper, Robert; Pfenning, Frank 17 2005 Structured theory presentations and logic representations. Zbl 0809.03019Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 16 1994 Computational higher-dimensional type theory. Zbl 1380.68112Angiuli, Carlo; Harper, Robert; Wilson, Todd 16 2017 Mechanizing metatheory in a logical framework. Zbl 1125.68029Harper, Robert; Licata, Daniel R. 14 2007 Syntactic logical relations for polymorphic and recursive types. Zbl 1277.68119Crary, Karl; Harper, Robert 11 2007 Extensional equivalence and singleton types. Zbl 1367.68055Stone, Christopher A.; Harper, Robert 9 2006 Deciding type equivalence in a language with singleton kinds. Zbl 1323.68163Stone, Christopher A.; Harper, Robert 9 2000 Type checking with universes. Zbl 0737.68013Harper, Robert; Pollack, Robert 8 1991 A type system for higher-order modules. Zbl 1321.68167Dreyer, Derek; Crary, Karl; Harper, Robert 8 2003 Distributed control flow with classical modal logic. Zbl 1136.68443Murphy, Tom VII; Crary, Karl; Harper, Robert 7 2005 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 7 2001 Cartesian cubical computational type theory: constructive reasoning with paths and equalities. Zbl 07533331Angiuli, Carlo; Hou, (Favonia) Kuen-Bang; Harper, Robert 7 2018 Corrigendum: Polymorphic type assignment and CPS conversion. Zbl 1058.68727Harper, Robert; Lillibridge, Mark 6 2003 A simplified account of polymorphic references. Zbl 0813.68131Harper, Robert 6 1994 Proof-directed debugging. Zbl 0948.68038Harper, Robert 6 1999 Structure and representation in LF. Zbl 0716.68078Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 6 1989 A dependently typed assembly language. Zbl 1323.68084Xi, Hongwei; Harper, Robert 6 2001 A higher-order logic for concurrent termination-preserving refinement. Zbl 1485.68076Tassarotti, Joseph; Jung, Ralf; Harper, Robert 5 2017 2-dimensional directed type theory. Zbl 1343.03051Licata, Daniel R.; Harper, Robert 5 2011 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. 5 1999 Verified tail bounds for randomized programs. Zbl 1511.68342Tassarotti, Joseph; Harper, Robert 5 2018 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 5 2004 A universe of binding and computation. Zbl 1302.68050Licata, Daniel R.; Harper, Robert 5 2009 Adaptive functional programming. Zbl 1322.68034Acar, Umut A.; Blelloch, Guy E.; Harper, Robert 5 2002 Syntax and models of Cartesian cubical type theory. Zbl 07460116Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Hou (Favonia), Kuen-Bang; Licata, Daniel R. 4 2021 Relational interpretations of recursive types in an operational setting. Zbl 0888.03016Birkedal, Lars; Harper, Robert 3 1997 Homotopical patch theory. Zbl 1420.68060Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert 3 2016 Meaning explanations at higher dimension. Zbl 1436.03102Angiuli, Carlo; Harper, Robert 3 2018 An effective theory of type refinements. Zbl 1315.68055Mandelbaum, Yitzhak; Walker, David; Harper, Robert 3 2003 Automatic generation of staged geometric predicates. Zbl 1323.68540Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert 3 2001 Modular type classes. Zbl 1295.68061Dreyer, Derek; Harper, Robert; Chakravarty, Manuel M. T.; Keller, Gabriele 3 2007 Logic representation in LF. Report on work in progress. Zbl 1496.03055Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 3 1989 Constructing type systems over an operational semantics. Zbl 0766.68088Harper, Robert 2 1992 Operational interpretations of an extension of \(F_ \omega\) with control operators. Zbl 0861.68055Harper, Robert; Lillibridge, Mark 2 1996 A note on “A simplified account of polymorphic references”. Zbl 0998.68534Harper, Robert 2 1996 A module system for a programming language based on the LF logical framework. Zbl 0902.68031Harper, Robert; Pfenning, Frank 2 1998 A type discipline for program modules. Zbl 0614.68010Harper, Robert; Milner, Robin; Tofte, Mads 2 1987 Internal parametricity for cubical type theory. Zbl 07650826Cavallo, Evan; Harper, Robert 1 2020 Homotopical patch theory. Zbl 1345.68093Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert 1 2014 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 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 Guarded computational type theory. Zbl 1453.03027Sterling, Jonathan; Harper, Robert 1 2018 Syntax and models of Cartesian cubical type theory. Zbl 07460116Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Hou (Favonia), Kuen-Bang; Licata, Daniel R. 4 2021 Internal parametricity for cubical type theory. Zbl 07650826Cavallo, Evan; Harper, Robert 1 2020 Cartesian cubical computational type theory: constructive reasoning with paths and equalities. Zbl 07533331Angiuli, Carlo; Hou, (Favonia) Kuen-Bang; Harper, Robert 7 2018 Verified tail bounds for randomized programs. Zbl 1511.68342Tassarotti, Joseph; Harper, Robert 5 2018 Meaning explanations at higher dimension. Zbl 1436.03102Angiuli, Carlo; Harper, Robert 3 2018 Guarded computational type theory. Zbl 1453.03027Sterling, Jonathan; Harper, Robert 1 2018 Computational higher-dimensional type theory. Zbl 1380.68112Angiuli, Carlo; Harper, Robert; Wilson, Todd 16 2017 A higher-order logic for concurrent termination-preserving refinement. Zbl 1485.68076Tassarotti, Joseph; Jung, Ralf; Harper, Robert 5 2017 Practical foundations for programming languages. 2nd edition. Zbl 1347.68001Harper, Robert 21 2016 Homotopical patch theory. Zbl 1420.68060Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert 3 2016 Homotopical patch theory. Zbl 1345.68093Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert 1 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 128 2013 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 5 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 20 2007 Mechanizing metatheory in a logical framework. Zbl 1125.68029Harper, Robert; Licata, Daniel R. 14 2007 Syntactic logical relations for polymorphic and recursive types. Zbl 1277.68119Crary, Karl; Harper, Robert 11 2007 Modular type classes. Zbl 1295.68061Dreyer, Derek; Harper, Robert; Chakravarty, Manuel M. T.; Keller, Gabriele 3 2007 Extensional equivalence and singleton types. Zbl 1367.68055Stone, Christopher A.; Harper, Robert 9 2006 On equivalence and canonical forms in the LF type theory. Zbl 1367.03055Harper, Robert; Pfenning, Frank 17 2005 Distributed control flow with classical modal logic. Zbl 1136.68443Murphy, Tom VII; Crary, Karl; Harper, Robert 7 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 5 2004 A type system for higher-order modules. Zbl 1321.68167Dreyer, Derek; Crary, Karl; Harper, Robert 8 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 Automatic generation of staged geometric predicates. Zbl 1059.68147Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert 1 2003 A type theory for memory allocation and data layout. Zbl 1321.68181Petersen, Leaf; Harper, Robert; Crary, Karl; Pfenning, Frank 1 2003 Adaptive functional programming. Zbl 1322.68034Acar, Umut A.; Blelloch, Guy E.; Harper, Robert 5 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 7 2001 A dependently typed assembly language. Zbl 1323.68084Xi, Hongwei; Harper, Robert 6 2001 Automatic generation of staged geometric predicates. Zbl 1323.68540Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert 3 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 9 2000 Proof-directed debugging. Zbl 0948.68038Harper, Robert 6 1999 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. 5 1999 A module system for a programming language based on the LF logical framework. Zbl 0902.68031Harper, Robert; Pfenning, Frank 2 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 Operational interpretations of an extension of \(F_ \omega\) with control operators. Zbl 0861.68055Harper, Robert; Lillibridge, Mark 2 1996 A note on “A simplified account of polymorphic references”. Zbl 0998.68534Harper, Robert 2 1996 Structured theory presentations and logic representations. Zbl 0809.03019Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 16 1994 A simplified account of polymorphic references. Zbl 0813.68131Harper, Robert 6 1994 A framework for defining logics. Zbl 0778.03004Harper, Robert; Honsell, Furio; Plotkin, Gordon 212 1993 Constructing type systems over an operational semantics. Zbl 0766.68088Harper, Robert 2 1992 Type checking with universes. Zbl 0737.68013Harper, Robert; Pollack, Robert 8 1991 Structure and representation in LF. Zbl 0716.68078Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 6 1989 Logic representation in LF. Report on work in progress. Zbl 1496.03055Harper, Robert; Sannella, Donald; Tarlecki, Andrzej 3 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 504 Authors 25 Rabe, Florian 17 Harper, Robert 16 Pientka, Brigitte 12 Kohlhase, Michael 10 Miller, Dale Allen 9 Abel, Andreas M. 9 Felty, Amy P. 8 Honsell, Furio 8 Pfenning, Frank 8 Tarlecki, Andrzej 7 Angiuli, Carlo 7 Horozal, Fulya 7 Momigliano, Alberto 6 Birkedal, Lars 6 Liquori, Luigi 6 Meseguer Guaita, José 6 Miculan, Marino 6 Nadathur, Gopalan 6 Roşu, Grigore 6 Sannella, Donald T. 5 Licata, Daniel R. 5 Luo, Zhaohui 5 Rossberg, Andreas 5 Scagnetto, Ivan 4 Buchholtz, Ulrik 4 Cheney, James 4 Coquand, Thierry 4 Crary, Karl 4 Diaconescu, Răzvan 4 Dreyer, Derek R. 4 Hou (Favonia), Kuen-Bang 4 Lenisa, Marina 4 Mossakowski, Till 4 Thiemann, Peter J. 3 Acar, Umut A. 3 Barthe, Gilles 3 Basin, David A. 3 Bauer, Andrej 3 Cervesato, Iliano 3 Ciaffaglione, Alberto 3 Duggan, Dominic 3 Gacek, Andrew 3 Geuvers, Jan Herman 3 Gratzer, Daniel 3 Hirschowitz, André 3 Iancu, Mihnea 3 Krebbers, Robbert 3 Maggesi, Marco 3 Paulson, Lawrence Charles 3 Pitts, Andrew M. 3 Pym, David J. 3 Sacerdoti Coen, Claudio 3 Schürmann, Carsten 3 Sterling, Jonathan 3 Toninho, Bernardo 3 Weirich, Stephanie 3 Yoshida, Nobuko 2 Adams, Robin 2 Ahrens, Benedikt 2 Anderson, Penny 2 Ariola, Zena M. 2 Atkey, Robert 2 Avron, Arnon 2 Benton, Nick 2 Bezem, Marc 2 Bizjak, Aleš 2 Blanqui, Frédéric 2 Bonelli, Eduardo 2 Cave, Andrew 2 Chen, Gang 2 Chihani, Zakaria 2 Codescu, Mihai 2 Cohen, Liron 2 Constable, Robert Lee 2 Crole, Roy L. 2 Despeyroux, Joëlle 2 Dowek, Gilles 2 Downen, Paul 2 Dunfield, Joshua 2 Farka, František 2 Feller, Federico 2 Filinski, Andrzej 2 Gallagher, John P. 2 Garrigue, Jacques 2 Gheri, Lorenzo 2 Haselwarter, Philipp G. 2 Hatcliff, John 2 Hennicker, Rolf 2 Hermant, Olivier 2 Hermenegildo, Manuel V. 2 Howe, Douglas J. 2 Jung, Ralf 2 Kaliszyk, Cezary 2 Klev, Ansten Mørch 2 Lafont, Ambroise 2 Matthes, Ralph 2 Matthews, Seán 2 McBride, Conor Thomas 2 Morehouse, Edward 2 Morrisett, Greg ...and 404 more Authors all top 5 Cited in 50 Serials 31 Theoretical Computer Science 31 Journal of Automated Reasoning 29 Journal of Functional Programming 20 Information and Computation 20 MSCS. Mathematical Structures in Computer Science 15 Logical Methods in Computer Science 9 Formal Aspects of Computing 5 Annals of Pure and Applied Logic 5 Higher-Order and Symbolic Computation 5 Theory and Practice of Logic Programming 4 Information Processing Letters 4 Journal of Computer Science and Technology 3 The Bulletin of Symbolic Logic 3 RAIRO. Theoretical Informatics and Applications 3 The Journal of Logic and Algebraic Programming 3 ACM Transactions on Computational Logic 3 Journal of Applied Logic 3 Journal of Logical and Algebraic Methods in Programming 2 Acta Informatica 2 Science of Computer Programming 2 Journal of Symbolic Computation 2 Discrete & Computational Geometry 2 Journal of Applied Non-Classical Logics 2 Logica Universalis 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 Journal of Pure and Applied Algebra 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 Indagationes Mathematicae. New Series 1 Formal Methods in System Design 1 Journal of Logic, Language and Information 1 Applied Categorical Structures 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 Games 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 334 Computer science (68-XX) 194 Mathematical logic and foundations (03-XX) 15 Category theory; homological algebra (18-XX) 10 Algebraic topology (55-XX) 3 Numerical analysis (65-XX) 2 History and biography (01-XX) 2 Combinatorics (05-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 General and overarching topics; collections (00-XX) 1 General algebraic systems (08-XX) 1 Manifolds and cell complexes (57-XX) 1 Quantum theory (81-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.