×

zbMATH — the first resource for mathematics

Harper, Robert

Compute Distance To:
Author ID: harper.robert Recent zbMATH articles by "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

Publications by Year

Citations contained in zbMATH

43 Publications have been cited 377 times in 312 Documents Cited by Year
A framework for defining logics. Zbl 0778.03004
Harper, Robert; Honsell, Furio; Plotkin, Gordon
183
1993
Towards a mechanized metatheory of Standard ML. Zbl 1295.68088
Lee, Daniel K.; Crary, Karl; Harper, Robert
16
2007
Structured theory presentations and logic representations. Zbl 0809.03019
Harper, Robert; Sannella, Donald; Tarlecki, Andrzej
15
1994
On equivalence and canonical forms in the LF type theory. Zbl 1367.03055
Harper, Robert; Pfenning, Frank
13
2005
Mechanizing metatheory in a logical framework. Zbl 1125.68029
Harper, Robert; Licata, Daniel R.
12
2007
Practical foundations for programming languages. 2nd edition. Zbl 1347.68001
Harper, Robert
9
2016
Syntactic logical relations for polymorphic and recursive types. Zbl 1277.68119
Crary, Karl; Harper, Robert
9
2007
A type system for higher-order modules. Zbl 1321.68167
Dreyer, Derek; Crary, Karl; Harper, Robert
7
2003
Deciding type equivalence in a language with singleton kinds. Zbl 1323.68163
Stone, Christopher A.; Harper, Robert
7
2000
Structure and representation in LF. Zbl 0716.68078
Harper, Robert; Sannella, Donald; Tarlecki, Andrzej
7
1989
Computational higher-dimensional type theory. Zbl 1380.68112
Angiuli, Carlo; Harper, Robert; Wilson, Todd
6
2017
Extensional equivalence and singleton types. Zbl 1367.68055
Stone, Christopher A.; Harper, Robert
6
2006
Distributed control flow with classical modal logic. Zbl 1136.68443
Murphy, Tom VII; Crary, Karl; Harper, Robert
6
2005
Corrigendum: Polymorphic type assignment and CPS conversion. Zbl 1058.68727
Harper, Robert; Lillibridge, Mark
6
2003
On the unusual effectiveness of logic in computer science. Zbl 0979.03033
Halpern, Joseph Y.; Harper, Robert; Immerman, Neil; Kolaitis, Phokion G.; Vardi, Moshe Y.; Vianu, Victor
6
2001
Type checking with universes. Zbl 0737.68013
Harper, Robert; Pollack, Robert
6
1991
A universe of binding and computation. Zbl 1302.68050
Licata, Daniel R.; Harper, Robert
5
2009
Relational interpretations of recursive types in an operational setting. Zbl 1045.68504
Birkedal, Lars; Harper, Robert
5
1999
A simplified account of polymorphic references. Zbl 0813.68131
Harper, Robert
5
1994
Dynamizing static algorithms, with applications to dynamic trees and history independence. Zbl 1318.68080
Acar, 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.68024
Harper, Robert; Mitchell, John C.
4
1999
Proof-directed debugging. Zbl 0948.68038
Harper, Robert
4
1999
An effective theory of type refinements. Zbl 1315.68055
Mandelbaum, Yitzhak; Walker, David; Harper, Robert
3
2003
Adaptive functional programming. Zbl 1322.68034
Acar, Umut A.; Blelloch, Guy E.; Harper, Robert
3
2002
A dependently typed assembly language. Zbl 1323.68084
Xi, Hongwei; Harper, Robert
3
2001
A module system for a programming language based on the LF logical framework. Zbl 0902.68031
Harper, Robert; Pfenning, Frank
3
1998
Relational interpretations of recursive types in an operational setting. Zbl 0888.03016
Birkedal, Lars; Harper, Robert
3
1997
2-dimensional directed type theory. Zbl 1343.03051
Licata, Daniel R.; Harper, Robert
2
2011
Modular type classes. Zbl 1295.68061
Dreyer, Derek; Harper, Robert; Chakravarty, Manuel M. T.; Keller, Gabriele
2
2007
Automatic generation of staged geometric predicates. Zbl 1323.68540
Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert
2
2001
A note on “A simplified account of polymorphic references”. Zbl 0998.68534
Harper, Robert
2
1996
A type discipline for program modules. Zbl 0614.68010
Harper, Robert; Milner, Robin; Tofte, Mads
2
1987
Verified tail bounds for randomized programs. Zbl 06947002
Tassarotti, Joseph; Harper, Robert
1
2018
Meaning explanations at higher dimension. Zbl 1436.03102
Angiuli, Carlo; Harper, Robert
1
2018
A higher-order logic for concurrent termination-preserving refinement. Zbl 06721348
Tassarotti, Joseph; Jung, Ralf; Harper, Robert
1
2017
Homotopical patch theory. Zbl 1345.68093
Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert
1
2014
Canonicity for 2-dimensional type theory. Zbl 1321.03049
Licata, Daniel R.; Harper, Robert
1
2012
A type theory for memory allocation and data layout. Zbl 1321.68181
Petersen, Leaf; Harper, Robert; Crary, Karl; Pfenning, Frank
1
2003
Automatic generation of staged geometric predicates. Zbl 1059.68147
Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert
1
2003
A network protocol stack in standard ML. Zbl 1017.68005
Biagioni, Edoardo; Harper, Robert; Lee, Peter
1
2001
Typed closure conversion for recursively-defined functions. (Extended abstract). Zbl 0925.68298
Morrisett, Greg; Harper, Robert
1
1997
Operational interpretations of an extension of \(F_ \omega\) with control operators. Zbl 0861.68055
Harper, Robert; Lillibridge, Mark
1
1996
Constructing type systems over an operational semantics. Zbl 0766.68088
Harper, Robert
1
1992
Verified tail bounds for randomized programs. Zbl 06947002
Tassarotti, Joseph; Harper, Robert
1
2018
Meaning explanations at higher dimension. Zbl 1436.03102
Angiuli, Carlo; Harper, Robert
1
2018
Computational higher-dimensional type theory. Zbl 1380.68112
Angiuli, Carlo; Harper, Robert; Wilson, Todd
6
2017
A higher-order logic for concurrent termination-preserving refinement. Zbl 06721348
Tassarotti, Joseph; Jung, Ralf; Harper, Robert
1
2017
Practical foundations for programming languages. 2nd edition. Zbl 1347.68001
Harper, Robert
9
2016
Homotopical patch theory. Zbl 1345.68093
Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert
1
2014
Canonicity for 2-dimensional type theory. Zbl 1321.03049
Licata, Daniel R.; Harper, Robert
1
2012
2-dimensional directed type theory. Zbl 1343.03051
Licata, Daniel R.; Harper, Robert
2
2011
A universe of binding and computation. Zbl 1302.68050
Licata, Daniel R.; Harper, Robert
5
2009
Towards a mechanized metatheory of Standard ML. Zbl 1295.68088
Lee, Daniel K.; Crary, Karl; Harper, Robert
16
2007
Mechanizing metatheory in a logical framework. Zbl 1125.68029
Harper, Robert; Licata, Daniel R.
12
2007
Syntactic logical relations for polymorphic and recursive types. Zbl 1277.68119
Crary, Karl; Harper, Robert
9
2007
Modular type classes. Zbl 1295.68061
Dreyer, Derek; Harper, Robert; Chakravarty, Manuel M. T.; Keller, Gabriele
2
2007
Extensional equivalence and singleton types. Zbl 1367.68055
Stone, Christopher A.; Harper, Robert
6
2006
On equivalence and canonical forms in the LF type theory. Zbl 1367.03055
Harper, Robert; Pfenning, Frank
13
2005
Distributed control flow with classical modal logic. Zbl 1136.68443
Murphy, Tom VII; Crary, Karl; Harper, Robert
6
2005
Dynamizing static algorithms, with applications to dynamic trees and history independence. Zbl 1318.68080
Acar, 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.68167
Dreyer, Derek; Crary, Karl; Harper, Robert
7
2003
Corrigendum: Polymorphic type assignment and CPS conversion. Zbl 1058.68727
Harper, Robert; Lillibridge, Mark
6
2003
An effective theory of type refinements. Zbl 1315.68055
Mandelbaum, Yitzhak; Walker, David; Harper, Robert
3
2003
A type theory for memory allocation and data layout. Zbl 1321.68181
Petersen, Leaf; Harper, Robert; Crary, Karl; Pfenning, Frank
1
2003
Automatic generation of staged geometric predicates. Zbl 1059.68147
Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert
1
2003
Adaptive functional programming. Zbl 1322.68034
Acar, Umut A.; Blelloch, Guy E.; Harper, Robert
3
2002
On the unusual effectiveness of logic in computer science. Zbl 0979.03033
Halpern, Joseph Y.; Harper, Robert; Immerman, Neil; Kolaitis, Phokion G.; Vardi, Moshe Y.; Vianu, Victor
6
2001
A dependently typed assembly language. Zbl 1323.68084
Xi, Hongwei; Harper, Robert
3
2001
Automatic generation of staged geometric predicates. Zbl 1323.68540
Nanevski, Aleksandar; Blelloch, Guy; Harper, Robert
2
2001
A network protocol stack in standard ML. Zbl 1017.68005
Biagioni, Edoardo; Harper, Robert; Lee, Peter
1
2001
Deciding type equivalence in a language with singleton kinds. Zbl 1323.68163
Stone, Christopher A.; Harper, Robert
7
2000
Relational interpretations of recursive types in an operational setting. Zbl 1045.68504
Birkedal, Lars; Harper, Robert
5
1999
Parametricity and variants of Girard’s \(J\) operator. Zbl 1002.68024
Harper, Robert; Mitchell, John C.
4
1999
Proof-directed debugging. Zbl 0948.68038
Harper, Robert
4
1999
A module system for a programming language based on the LF logical framework. Zbl 0902.68031
Harper, Robert; Pfenning, Frank
3
1998
Relational interpretations of recursive types in an operational setting. Zbl 0888.03016
Birkedal, Lars; Harper, Robert
3
1997
Typed closure conversion for recursively-defined functions. (Extended abstract). Zbl 0925.68298
Morrisett, Greg; Harper, Robert
1
1997
A note on “A simplified account of polymorphic references”. Zbl 0998.68534
Harper, Robert
2
1996
Operational interpretations of an extension of \(F_ \omega\) with control operators. Zbl 0861.68055
Harper, Robert; Lillibridge, Mark
1
1996
Structured theory presentations and logic representations. Zbl 0809.03019
Harper, Robert; Sannella, Donald; Tarlecki, Andrzej
15
1994
A simplified account of polymorphic references. Zbl 0813.68131
Harper, Robert
5
1994
A framework for defining logics. Zbl 0778.03004
Harper, Robert; Honsell, Furio; Plotkin, Gordon
183
1993
Constructing type systems over an operational semantics. Zbl 0766.68088
Harper, Robert
1
1992
Type checking with universes. Zbl 0737.68013
Harper, Robert; Pollack, Robert
6
1991
Structure and representation in LF. Zbl 0716.68078
Harper, Robert; Sannella, Donald; Tarlecki, Andrzej
7
1989
A type discipline for program modules. Zbl 0614.68010
Harper, Robert; Milner, Robin; Tofte, Mads
2
1987
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

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.