default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDRobert Harper 0001
Robert William Harper Jr.
Person information
- affiliation (since 1988): Carnegie Mellon University, School of Computer Science, Pittsburgh, USA
- affiliation (1985 - 1988): University of Edinburgh, Laboratory for Foundations of Computer Science, UK
Other persons with the same name
- Robert Harper 0002 — Oculus Info Inc., Toronto, ON, Canada
- Robert Harper 0003 — University of Manchester, School of Medicine, UK
- Robert Harper 0004
![[0000-0002-3269-3273]](https://dblp.uni-trier.de./img/orcid-mark.12x12.png "0000-0002-3269-3273")
— Moogsoft Ltd, Kingston-Upon-Thames, UK - Robert Harper 0005 — University College London, Mullard Space Science Laboratory, Surrey, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j48]Harrison Grodin, Yue Niu, Jonathan Sterling, Robert Harper:
Decalf: A Directed, Effectful Cost-Aware Logical Framework. Proc. ACM Program. Lang. 8(POPL): 273-301 (2024)- [i27]Yue Niu, Jonathan Sterling, Robert Harper:
Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory. CoRR abs/2404.00212 (2024) - [i26]Harrison Grodin, Robert Harper:
Amortized Analysis via Coalgebra. CoRR abs/2404.03641 (2024) - 2023
- [c79]Robert Harper:
Integrating Cost and Behavior in Type Theory (Invited Talk). CALCO 2023: 1:1-1:2 - [c78]Harrison Grodin, Robert Harper:
Amortized Analysis via Coinduction (Early Ideas). CALCO 2023: 23:1-23:6 - [c77]Yue Niu, Robert Harper:
A Metalanguage for Cost-Aware Denotational Semantics. LICS 2023: 1-14 - [i25]Harrison Grodin, Robert Harper:
Amortized Analysis via Coinduction. CoRR abs/2303.16048 (2023) - [i24]Harrison Grodin, Robert Harper, Yue Niu, Jonathan Sterling:
Decalf: A Directed, Effectful Cost-Aware Logical Framework. CoRR abs/2307.05938 (2023) - [i23]Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao:
Logical Relations for Session-Typed Concurrency. CoRR abs/2309.00192 (2023) - [i22]Runming Li, Harrison Grodin, Robert Harper:
A Verified Cost Analysis of Joinable Red-Black Trees. CoRR abs/2309.11056 (2023) - 2022
- [j47]Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper:
A cost-aware logical framework. Proc. ACM Program. Lang. 6(POPL): 1-31 (2022) - [c76]Jonathan Sterling, Robert Harper:
Sheaf Semantics of Termination-Insensitive Noninterference. FSCD 2022: 5:1-5:19 - [i21]Jonathan Sterling, Robert Harper:
Sheaf semantics of termination-insensitive noninterference. CoRR abs/2204.09421 (2022) - [i20]Yue Niu, Robert Harper:
A metalanguage for cost-aware denotational semantics. CoRR abs/2209.12669 (2022) - 2021
- [j46]Jonathan Sterling, Robert Harper:
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. J. ACM 68(6): 41:1-41:47 (2021) - [j45]Evan Cavallo, Robert Harper:
Internal Parametricity for Cubical Type Theory. Log. Methods Comput. Sci. 17(4) (2021) - [j44]Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata:
Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. 31(4): 424-468 (2021) - [i19]Robert Harper:
An Equational Logical Framework for Type Theories. CoRR abs/2106.01484 (2021) - [i18]Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper:
A cost-aware logical framework. CoRR abs/2107.04663 (2021) - 2020
- [j43]David MacQueen, Robert Harper, John H. Reppy:
The history of Standard ML. Proc. ACM Program. Lang. 4(HOPL): 86:1-86:100 (2020) - [c75]Evan Cavallo, Robert Harper:
Internal Parametricity for Cubical Type Theory. CSL 2020: 13:1-13:17 - [i17]Evan Cavallo, Robert Harper:
Internal Parametricity for Cubical Type Theory. CoRR abs/2005.11290 (2020) - [i16]Jonathan Sterling, Robert Harper:
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. CoRR abs/2010.08599 (2020) - [i15]Yue Niu, Robert Harper:
Cost-Aware Type Theory. CoRR abs/2011.03660 (2020)
2010 – 2019
- 2019
- [j42]Evan Cavallo, Robert Harper:
Higher inductive types in cubical computational type theory. Proc. ACM Program. Lang. 3(POPL): 1:1-1:27 (2019) - [j41]Joseph Tassarotti, Robert Harper:
A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3(POPL): 64:1-64:30 (2019) - [i14]Evan Cavallo, Robert Harper:
Parametric Cubical Type Theory. CoRR abs/1901.00489 (2019) - 2018
- [j40]Stefan K. Muller, Umut A. Acar, Robert Harper:
Competitive parallelism: getting your priorities right. Proc. ACM Program. Lang. 2(ICFP): 95:1-95:30 (2018) - [j39]Robert Harper:
Exception tracking in an open world. Theor. Comput. Sci. 741: 25-31 (2018) - [c74]Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper:
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. CSL 2018: 6:1-6:17 - [c73]Joseph Tassarotti, Robert Harper:
Verified Tail Bounds for Randomized Programs. ITP 2018: 560-578 - [c72]Jonathan Sterling, Robert Harper:
Guarded Computational Type Theory. LICS 2018: 879-888 - [c71]Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, Jonathan Sterling:
The RedPRL Proof Assistant (Invited Paper). LFMTP@FSCD 2018: 1-10 - [i13]Evan Cavallo, Robert Harper:
Computational Higher Type Theory IV: Inductive Types. CoRR abs/1801.01568 (2018) - [i12]Joseph Tassarotti, Robert Harper:
A Separation Logic for Concurrent Randomized Programs. CoRR abs/1802.02951 (2018) - [i11]Jonathan Sterling, Robert Harper:
Guarded Computational Type Theory. CoRR abs/1804.09098 (2018) - [i10]Stefan K. Muller, Umut A. Acar, Robert Harper:
Competitive Parallelism: Getting Your Priorities Right. CoRR abs/1807.03703 (2018) - 2017
- [j38]Kuen-Bang Hou (Favonia), Nick Benton, Robert Harper:
Correctness of compiling polymorphism to dynamic typing. J. Funct. Program. 27: e1 (2017) - [c70]Joseph Tassarotti, Ralf Jung, Robert Harper:
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. ESOP 2017: 909-936 - [c69]Stefan K. Muller, Umut A. Acar, Robert Harper:
Responsive parallel computation: bridging competitive and cooperative threading. PLDI 2017: 677-692 - [c68]Carlo Angiuli, Robert Harper, Todd Wilson:
Computational higher-dimensional type theory. POPL 2017: 680-693 - [c67]Ananya Kumar, Guy E. Blelloch, Robert Harper:
Parallel functional arrays. POPL 2017: 706-718 - [i9]Joseph Tassarotti, Ralf Jung, Robert Harper:
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. CoRR abs/1701.05888 (2017) - [i8]Jonathan Sterling, Robert Harper:
Algebraic Foundations of Proof Refinement. CoRR abs/1703.05215 (2017) - [i7]Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper:
Computational Higher Type Theory III: Univalent Universes and Exact Equality. CoRR abs/1712.01800 (2017) - 2016
- [b4]Robert Harper:
Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press 2016, ISBN 9781107150300 - [j37]Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper:
Homotopical patch theory. J. Funct. Program. 26: e18 (2016) - [c66]Kuen-Bang Hou (Favonia), Robert Harper:
Covering Spaces in Homotopy Type Theory. TYPES 2016: 11:1-11:16 - [i6]Carlo Angiuli, Robert Harper, Todd Wilson:
Computational Higher Type Theory I: Abstract Cubical Realizability. CoRR abs/1604.08873 (2016) - [i5]Carlo Angiuli, Robert Harper:
Computational Higher Type Theory II: Dependent Cubical Realizability. CoRR abs/1606.09638 (2016) - 2015
- [j36]Guy E. Blelloch, Robert Harper:
Cache efficient functional algorithms. Commun. ACM 58(7): 101-108 (2015) - [j35]Steve Awodey, Robert Harper:
Homotopy type theory: unified foundations of mathematics and computation. ACM SIGLOG News 2(1): 37-44 (2015) - [i4]Robert Harper, Kuen-Bang Hou (Favonia):
A Note on the Uniform Kan Condition in Nominal Cubical Sets. CoRR abs/1501.05691 (2015) - 2014
- [c65]Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper:
Homotopical patch theory. ICFP 2014: 243-256 - 2013
- [c64]Guy E. Blelloch, Robert Harper:
Cache and I/O efficent functional algorithms. POPL 2013: 39-50 - 2012
- [c63]Daniel R. Licata, Robert Harper:
Canonicity for 2-dimensional type theory. POPL 2012: 337-348 - 2011
- [c62]Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell:
Robin Milner 1934--2010: verification, languages, and concurrency. POPL 2011: 473-474 - [c61]Daniel R. Licata, Robert Harper:
2-Dimensional Directed Type Theory. MFPS 2011: 263-289 - [i3]Umut A. Acar, Guy E. Blelloch, Robert Harper:
Selective Memoization. CoRR abs/1106.0447 (2011) - 2010
- [j34]Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons:
Space profiling for parallel functional programs. J. Funct. Program. 20(5-6): 417-461 (2010) - [c60]Kumar Avijit, Anupam Datta, Robert Harper:
Distributed programming with distributed authorization. TLDI 2010: 27-38 - [c59]Daniel R. Licata, Robert Harper:
A Monadic Formalization of ML5. LFMTP 2010: 69-83
2000 – 2009
- 2009
- [j33]Robert Harper:
FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum. J. Funct. Program. 19(2): 262 (2009) - [j32]Jim Allen, Zena M. Ariola, Pierre-Louis Curien, Matthew Fluet, Jeffrey S. Foster, Dan Grossman, Robert Harper, Hugo Herbelin, Yannis Smaragdakis, David Walker, Steve Zdancewic:
An overview of the Oregon programming languages summer school. ACM SIGPLAN Notices 44(11): 1-3 (2009) - [j31]Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan:
An experimental analysis of self-adjusting computation. ACM Trans. Program. Lang. Syst. 32(1): 3:1-3:53 (2009) - [c58]Daniel R. Licata, Robert Harper:
A universe of binding and computation. ICFP 2009: 123-134 - [c57]Daniel R. Licata, Robert Harper:
Positively dependent types. PLPV 2009: 3-14 - [c56]Mark W. Bailey, Kim B. Bruce, Kathleen Fisher, Robert Harper, Stuart Reges:
Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report. SIGCSE 2009: 132-133 - [c55]Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, Robert Harper:
Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures. SPAA 2009: 91-100 - [c54]Robert Harper, Daniel R. Licata, Noam Zeilberger:
A Pronominal Approach to Binding and Computation. TLCA 2009: 3-4 - 2008
- [j30]Eric Allen, Mark W. Bailey, Rastislav Bodík, Kim B. Bruce, Kathleen Fisher, Stephen N. Freund, Robert Harper, Chandra Krintz, Shriram Krishnamurthi, James R. Larus, Doug Lea, Gary T. Leavens, Lori L. Pollock, Stuart Reges, Martin C. Rinard, Mark A. Sheldon, Franklyn A. Turbak, Mitchell Wand:
SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations. ACM SIGPLAN Notices 43(11): 6-29 (2008) - [j29]Robert Harper:
Position paper: practical foundations for lrogramming languages. ACM SIGPLAN Notices 43(11): 71-73 (2008) - [c53]Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons:
Space profiling for parallel functional programs. ICFP 2008: 253-264 - [c52]Daniel R. Licata, Noam Zeilberger, Robert Harper:
Focusing on Binding and Computation. LICS 2008: 241-252 - 2007
- [j28]Robert Harper, Daniel R. Licata:
Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4-5): 613-673 (2007) - [c51]Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller:
Modular type classes. POPL 2007: 63-70 - [c50]Daniel K. Lee, Karl Crary, Robert Harper:
Towards a mechanized metatheory of standard ML. POPL 2007: 173-184 - [c49]Tom Murphy VII, Karl Crary, Robert Harper:
Type-Safe Distributed Programming with ML5. TGC 2007: 108-123 - [c48]Karl Crary, Robert Harper:
Syntactic Logical Relations for Polymorphic and Recursive Types. Computation, Meaning, and Logic 2007: 259-299 - 2006
- [j27]Karl Crary, Robert Harper:
Higher-order abstract syntax: setting the record straight. SIGACT News 37(3): 93-96 (2006) - [j26]Christopher A. Stone, Robert Harper:
Extensional equivalence and singleton types. ACM Trans. Comput. Log. 7(4): 676-722 (2006) - [j25]Umut A. Acar, Guy E. Blelloch, Robert Harper:
Adaptive functional programming. ACM Trans. Program. Lang. Syst. 28(6): 990-1034 (2006) - [c47]David Swasey, Tom Murphy VII, Karl Crary, Robert Harper:
A separate compilation extension to standard ML. ML 2006: 32-42 - [i2]Karl Crary, Robert Harper:
Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight. CoRR abs/cs/0607141 (2006) - 2005
- [j24]Robert Harper, Frank Pfenning:
On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. 6(1): 61-101 (2005) - [c46]Tom Murphy VII, Karl Crary, Robert Harper:
Distributed Control Flow with Classical Modal Logic. CSL 2005: 51-69 - [c45]Robert Harper:
Mechanizing the meta-theory of programming languages. ICFP 2005: 240 - [c44]Adam Chlipala, Leaf Petersen, Robert Harper:
Strict bidirectional type checking. TLDI 2005: 71-78 - [c43]Daniel Spoonhower, Guy E. Blelloch, Robert Harper:
Using page residency to balance tradeoffs in tracing garbage collection. VEE 2005: 57-67 - [c42]Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan:
A Library for Self-Adjusting Computation. ML 2005: 127-154 - 2004
- [j23]David A. Basin, Olivier Danvy, Robert Harper:
Editorial. High. Order Symb. Comput. 17(3): 171 (2004) - [c41]Robert Harper:
Self-Adjusting Computation. ICALP 2004: 1-2 - [c40]Robert Harper, M. Ed Jernigan:
Self-adjusting beat detection and prediction in music. ICASSP (4) 2004: 245-248 - [c39]Robert Harper:
Self-Adjusting Computation. LICS 2004: 254-255 - [c38]Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning:
A Symmetric Modal Lambda Calculus for Distributed Computing. LICS 2004: 286-295 - [c37]Umut A. Acar, Guy E. Blelloch, Robert Harper, Jorge L. Vittes, Shan Leung Maverick Woo:
Dynamizing static algorithms, with applications to dynamic trees and history independence. SODA 2004: 531-540 - 2003
- [j22]Aleksandar Nanevski, Guy E. Blelloch, Robert Harper:
Automatic Generation of Staged Geometric Predicates. High. Order Symb. Comput. 16(4): 379-400 (2003) - [j21]Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning:
Automated techniques for provably safe mobile code. Theor. Comput. Sci. 290(2): 1175-1199 (2003) - [c36]Yitzhak Mandelbaum, David Walker, Robert Harper:
An effective theory of type refinements. ICFP 2003: 213-225 - [c35]Umut A. Acar, Guy E. Blelloch, Robert Harper:
Selective memoization. POPL 2003: 14-25 - [c34]Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning:
A type theory for memory allocation and data layout. POPL 2003: 172-184 - [c33]Derek Dreyer, Karl Crary, Robert Harper:
A type system for higher-order modules. POPL 2003: 236-249 - [c32]Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng:
Typed compilation of recursive datatypes. TLDI 2003: 98-108 - 2002
- [c31]Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning:
Trustless Grid Computing in ConCert. GRID 2002: 112-125 - [c30]Umut A. Acar, Guy E. Blelloch, Robert Harper:
Adaptive functional programming. POPL 2002: 247-259 - 2001
- [j20]Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, Victor Vianu:
On the unusual effectiveness of logic in computer science. Bull. Symb. Log. 7(2): 213-236 (2001) - [j19]Guy E. Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary L. Miller, Noel Walkington:
Persistent triangulations Journal of Functional Programming. J. Funct. Program. 11(5): 441-466 (2001) - [j18]Edoardo Biagioni, Robert Harper, Peter Lee:
A Network Protocol Stack in Standard ML. High. Order Symb. Comput. 14(4): 309-356 (2001) - [c29]Fred B. Schneider, J. Gregory Morrisett, Robert Harper:
A Language-Based Approach to Security. Informatics 2001: 86-101 - [c28]Hongwei Xi, Robert Harper:
A Dependently Typed Assembly Language. ICFP 2001: 169-180 - [c27]Aleksandar Nanevski, Guy E. Blelloch, Robert Harper:
Automatic Generation of Staged Geometric Predicates. ICFP 2001: 217-228 - [e2]Robert Harper:
Types in Compilation, Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000, Revised Selected Papers. Lecture Notes in Computer Science 2071, Springer 2001, ISBN 3-540-42196-3 [contents] - [i1]Robert Harper, Frank Pfenning:
On Equivalence and Canonical Forms in the LF Type Theory. CoRR cs.LO/0110028 (2001) - 2000
- [c26]Robert Harper, Christopher A. Stone:
A type-theoretic interpretation of standard ML. Proof, Language, and Interaction 2000: 341-388 - [c25]Robert Harper, Benjamin C. Pierce:
Advanced module systems: a guide for the perplexed (abstract of invited talk). ICFP 2000: 130 - [c24]Christopher A. Stone, Robert Harper:
Deciding Type Equivalence with Singleton Kinds. POPL 2000: 214-227
1990 – 1999
- 1999
- [j17]Lars Birkedal, Robert Harper:
Relational Interpretations of Recursive Types in an Operational Setting. Inf. Comput. 155(1-2): 3-63 (1999) - [j16]Robert Harper, John C. Mitchell:
Parametricity and Variants of Girard's J Operator. Inf. Process. Lett. 70(1): 1-5 (1999) - [j15]Robert Harper:
Proof-Directed Debugging. J. Funct. Program. 9(4): 463-469 (1999) - [c23]Karl Crary, Robert Harper, Sidd Puri:
What is a Recursive Module? PLDI 1999: 50-63 - 1998
- [j14]Robert Harper, Frank Pfenning:
A Module System for a Programming Language Based on the LF Logical Framework. J. Log. Comput. 8(1): 5-31 (1998) - [c22]Perry Cheng, Robert Harper, Peter Lee:
Generational Stack Collection and Profile-Driven Pretenuring. PLDI 1998: 162-173 - [c21]Andrew Bernard, Robert Harper, Peter Lee:
How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler. Types in Compilation 1998: 53-77 - 1997
- [j13]Robert Harper, John C. Mitchell:
ML and Beyond. ACM SIGPLAN Notices 32(1): 80-85 (1997) - [c20]Lars Birkedal, Robert Harper:
Relational Interpretations of Recursive Types in an operational Setting (Summary). TACS 1997: 458-490 - [c19]J. Gregory Morrisett, Robert Harper:
Typed Closure Conversion for Recursively-Defined Functions. HOOTS 1997: 230-241 - 1996
- [j12]Robert Harper, Peter Lee:
Research in Programming Languages for Composability, Safety, and Performance. ACM Comput. Surv. 28(4es): 195 (1996) - [j11]Robert Harper, John C. Mitchell:
ML and Beyond. ACM Comput. Surv. 28(4es): 219 (1996) - [j10]Robert Harper:
A Note on "A Simplified Account of Polymorphic References". Inf. Process. Lett. 57(1): 15-16 (1996) - [j9]Robert Harper, Mark Lillibridge:
Operational Interpretations of an Extension of Fomega with Control Operators. J. Funct. Program. 6(3): 393-417 (1996) - [c18]David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee:
TIL: A Type-Directed Optimizing Compiler for ML. PLDI 1996: 181-192 - [c17]David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee:
TIL: a type-directed, optimizing compiler for ML (with retrospective). Best of PLDI 1996: 554-567 - [c16]Yasuhiko Minamide, J. Gregory Morrisett, Robert Harper:
Typed Closure Conversion. POPL 1996: 271-283 - [e1]Robert Harper, Richard L. Wexelblat:
Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, Philadelphia, Pennsylvania, USA, May 24-26, 1996. ACM 1996, ISBN 0-89791-770-7 [contents] - 1995
- [c15]J. Gregory Morrisett, Matthias Felleisen, Robert Harper:
Abstract Models of Memory Management. FPCA 1995: 66-77 - [c14]Robert Harper, J. Gregory Morrisett:
Compiling Polymorphism Using Intensional Type Analysis. POPL 1995: 130-141 - 1994
- [j8]Robert Harper, Donald Sannella, Andrzej Tarlecki:
Structured Theory Presentations and Logic Representations. Ann. Pure Appl. Log. 67(1-3): 113-160 (1994) - [j7]Robert Harper:
A Simplified Account of Polymorphic References. Inf. Process. Lett. 51(4): 201-206 (1994) - [c13]Edoardo Biagioni, Robert Harper, Peter Lee, Brian Milnes:
Signatures for a Network Protocol Stack: A Systems Application of Standard ML. LISP and Functional Programming 1994: 55-64 - [c12]Robert Harper, Mark Lillibridge:
A Type-Theoretic Approach to Higher-Order Modules with Sharing. POPL 1994: 123-137 - 1993
- [j6]Robert Harper, Furio Honsell, Gordon D. Plotkin:
A Framework for Defining Logics. J. ACM 40(1): 143-184 (1993) - [j5]Robert Harper, Bruce F. Duba, David B. MacQueen:
Typing First-Class Continuations in ML. J. Funct. Program. 3(4): 465-484 (1993) - [j4]Robert Harper, Mark Lillibridge:
Polymorphic Type Assignment and CPS Conversion. LISP Symb. Comput. 6(3-4): 361-380 (1993) - [j3]Robert Harper, John C. Mitchell:
On the Type Structure of Standard ML. ACM Trans. Program. Lang. Syst. 15(2): 211-252 (1993) - [c11]Robert Harper, Mark Lillibridge:
Explicit Polymorphism and CPS Conversion. POPL 1993: 206-219 - 1992
- [j2]Robert Harper:
Constructing Type Systems over an Operational Semantics. J. Symb. Comput. 14(1): 71-84 (1992) - 1991
- [j1]Robert Harper, Robert Pollack:
Type Checking with Universes. Theor. Comput. Sci. 89(1): 107-136 (1991) - [c10]Robert Harper, Benjamin C. Pierce:
A Record Calculus Based on Symmetric Concatenation. POPL 1991: 131-142 - [c9]Bruce F. Duba, Robert Harper, David B. MacQueen:
Typing First-Class Continuations in ML. POPL 1991: 163-173 - 1990
- [b3]Robin Milner, Mads Tofte, Robert Harper:
Definition of standard ML. MIT Press 1990, ISBN 978-0-262-63132-7, pp. I-XI, 1-101 - [c8]Robert Harper, John C. Mitchell, Eugenio Moggi:
Higher-Order Modules and the Phase Distinction. POPL 1990: 341-354
1980 – 1989
- 1989
- [c7]Robert Harper, Donald Sannella, Andrzej Tarlecki:
Logic Representation in LF. Category Theory and Computer Science 1989: 250-272 - [c6]Robert Harper, Donald Sannella, Andrzej Tarlecki:
Structure and Representation in LF. LICS 1989: 226-237 - [c5]Robert Harper, Robert Pollack:
Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft). TAPSOFT, Vol.2 1989: 241-256 - 1988
- [c4]John C. Mitchell, Robert Harper:
The Essence of ML. POPL 1988: 28-46 - 1987
- [c3]Robert Harper, Furio Honsell, Gordon D. Plotkin:
A Framework for Defining Logics. LICS 1987: 194-204 - [c2]Robert Harper, Robin Milner, Mads Tofte:
A Type Discipline for Program Modules. TAPSOFT, Vol.2 1987: 308-319 - 1986
- [b2]Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper, Douglas J. Howe, Todd B. Knoblock, Nax Paul Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith:
Implementing mathematics with the Nuprl proof development system. Prentice Hall 1986, ISBN 978-0-13-451832-9, pp. I-X, 1-299 - 1985
- [b1]Robert Harper:
Aspects of the Implementation of Type Theory. Cornell University, USA, 1985 - [c1]Robert Harper:
Modules and Persistence in Standard ML. Data Types and Persistence (Appin) 1985: 21-30
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-21 00:24 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
