| 2007 |
| 82 | EE | Daniel K. Lee,
Karl Crary,
Robert Harper:
Towards a mechanized metatheory of standard ML.
POPL 2007: 173-184 |
| 81 | EE | Derek Dreyer,
Robert Harper,
Manuel M. T. Chakravarty,
Gabriele Keller:
Modular type classes.
POPL 2007: 63-70 |
| 80 | EE | Tom Murphy VII,
Karl Crary,
Robert Harper:
Type-Safe Distributed Programming with ML5.
TGC 2007: 108-123 |
| 79 | EE | Karl Crary,
Robert Harper:
Syntactic Logical Relations for Polymorphic and Recursive Types.
Electr. Notes Theor. Comput. Sci. 172: 259-299 (2007) |
| 78 | EE | Pascale Proulx,
Lynn Chien,
Robert Harper,
David Schroh,
Thomas Kapler,
David Jonker,
William Wright:
nSpace and GeoTime: A VAST 2006 Case Study.
IEEE Computer Graphics and Applications 27(5): 46-56 (2007) |
| 2006 |
| 77 | EE | John Ainsworth,
Robert Harper,
Ismael Juma,
Iain E. Buchan:
PsyGrid: Applying e-Science to Epidemiology.
CBMS 2006: 727-732 |
| 76 | EE | David Swasey,
Tom Murphy VII,
Karl Crary,
Robert Harper:
A separate compilation extension to standard ML.
ML 2006: 32-42 |
| 75 | EE | Christopher A. Stone,
Robert Harper:
Extensional equivalence and singleton types.
ACM Trans. Comput. Log. 7(4): 676-722 (2006) |
| 74 | EE | Umut A. Acar,
Guy E. Blelloch,
Robert Harper:
Adaptive functional programming.
ACM Trans. Program. Lang. Syst. 28(6): 990-1034 (2006) |
| 73 | EE | Karl Crary,
Robert Harper:
Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight
CoRR abs/cs/0607141: (2006) |
| 72 | EE | Umut A. Acar,
Guy E. Blelloch,
Matthias Blume,
Robert Harper,
Kanat Tangwongsan:
A Library for Self-Adjusting Computation.
Electr. Notes Theor. Comput. Sci. 148(2): 127-154 (2006) |
| 71 | EE | Karl Crary,
Robert Harper:
Higher-order abstract syntax: setting the record straight.
SIGACT News 37(3): 93-96 (2006) |
| 2005 |
| 70 | EE | Tom Murphy VII,
Karl Crary,
Robert Harper:
Distributed Control Flow with Classical Modal Logic.
CSL 2005: 51-69 |
| 69 | EE | Robert Harper:
Mechanizing the meta-theory of programming languages.
ICFP 2005: 240 |
| 68 | EE | Adam J. Chlipala,
Leaf Petersen,
Robert Harper:
Strict bidirectional type checking.
TLDI 2005: 71-78 |
| 67 | EE | Daniel Spoonhower,
Guy E. Blelloch,
Robert Harper:
Using page residency to balance tradeoffs in tracing garbage collection.
VEE 2005: 57-67 |
| 66 | EE | Robert Harper,
Frank Pfenning:
On equivalence and canonical forms in the LF type theory.
ACM Trans. Comput. Log. 6(1): 61-101 (2005) |
| 2004 |
| 65 | EE | Robert Harper:
Self-Adjusting Computation.
ICALP 2004: 1-2 |
| 64 | EE | Robert Harper:
Self-Adjusting Computation.
LICS 2004: 254-255 |
| 63 | EE | Tom Murphy VII,
Karl Crary,
Robert Harper,
Frank Pfenning:
A Symmetric Modal Lambda Calculus for Distributed Computing.
LICS 2004: 286-295 |
| 62 | EE | 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 |
| 61 | EE | David A. Basin,
Olivier Danvy,
Robert Harper:
Editorial.
Higher-Order and Symbolic Computation 17(3): 171-171 (2004) |
| 2003 |
| 60 | EE | Yitzhak Mandelbaum,
David Walker,
Robert Harper:
An effective theory of type refinements.
ICFP 2003: 213-225 |
| 59 | EE | Umut A. Acar,
Guy E. Blelloch,
Robert Harper:
Selective memoization.
POPL 2003: 14-25 |
| 58 | EE | Leaf Petersen,
Robert Harper,
Karl Crary,
Frank Pfenning:
A type theory for memory allocation and data layout.
POPL 2003: 172-184 |
| 57 | EE | Derek Dreyer,
Karl Crary,
Robert Harper:
A type system for higher-order modules.
POPL 2003: 236-249 |
| 56 | EE | Joseph Vanderwaart,
Derek Dreyer,
Leaf Petersen,
Karl Crary,
Robert Harper,
Perry Cheng:
Typed compilation of recursive datatypes.
TLDI 2003: 98-108 |
| 55 | EE | Joseph Vanderwaart,
Derek Dreyer,
Leaf Petersen,
Karl Crary,
Robert Harper,
Perry Cheng:
Typed compilation of recursive datatypes.
TLDI 2003: 98-108 |
| 54 | EE | Aleksandar Nanevski,
Guy E. Blelloch,
Robert Harper:
Automatic Generation of Staged Geometric Predicates.
Higher-Order and Symbolic Computation 16(4): 379-400 (2003) |
| 53 | | 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) |
| 2002 |
| 52 | EE | 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 |
| 51 | EE | Umut A. Acar,
Guy E. Blelloch,
Robert Harper:
Adaptive functional programming.
POPL 2002: 247-259 |
| 2001 |
| 50 | | Robert Harper:
Types in Compilation, Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000, Revised Selected Papers
Springer 2001 |
| 49 | | Hongwei Xi,
Robert Harper:
A Dependently Typed Assembly Language.
ICFP 2001: 169-180 |
| 48 | | Aleksandar Nanevski,
Guy E. Blelloch,
Robert Harper:
Automatic Generation of Staged Geometric Predicates.
ICFP 2001: 217-228 |
| 47 | EE | Fred B. Schneider,
J. Gregory Morrisett,
Robert Harper:
A Language-Based Approach to Security.
Informatics 2001: 86-101 |
| 46 | EE | Joseph Y. Halpern,
Robert Harper,
Neil Immerman,
Phokion G. Kolaitis,
Moshe Y. Vardi,
Victor Vianu:
On the unusual effectiveness of logic in computer science.
Bulletin of Symbolic Logic 7(2): 213-236 (2001) |
| 45 | EE | Robert Harper,
Frank Pfenning:
On Equivalence and Canonical Forms in the LF Type Theory
CoRR cs.LO/0110028: (2001) |
| 44 | | Edoardo Biagioni,
Robert Harper,
Peter Lee:
A Network Protocol Stack in Standard ML.
Higher-Order and Symbolic Computation 14(4): 309-356 (2001) |
| 43 | | 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) |
| 2000 |
| 42 | EE | Robert Harper,
Benjamin C. Pierce:
Advanced module systems: a guide for the perplexed (abstract of invited talk).
ICFP 2000: 130 |
| 41 | EE | Christopher A. Stone,
Robert Harper:
Deciding Type Equivalence with Singleton Kinds.
POPL 2000: 214-227 |
| 1999 |
| 40 | EE | Karl Crary,
Robert Harper,
Sidd Puri:
What is a Recursive Module?
PLDI 1999: 50-63 |
| 39 | | Lars Birkedal,
Robert Harper:
Relational Interpretations of Recursive Types in an Operational Setting.
Inf. Comput. 155(1-2): 3-63 (1999) |
| 38 | EE | Robert Harper,
John C. Mitchell:
Parametricity and Variants of Girard's J Operator.
Inf. Process. Lett. 70(1): 1-5 (1999) |
| 37 | | Robert Harper:
Proof-Directed Debugging.
J. Funct. Program. 9(4): 463-469 (1999) |
| 1998 |
| 36 | | Perry Cheng,
Robert Harper,
Peter Lee:
Generational Stack Collection and Profile-Driven Pretenuring.
PLDI 1998: 162-173 |
| 35 | EE | 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 |
| 34 | | 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) |
| 1997 |
| 33 | | Lars Birkedal,
Robert Harper:
Relational Interpretations of Recursive Types in an operational Setting (Summary).
TACS 1997: 458-490 |
| 32 | EE | J. Gregory Morrisett,
Robert Harper:
Typed Closure Conversion for Recursively-Defined Functions.
Electr. Notes Theor. Comput. Sci. 10: (1997) |
| 31 | | Robert Harper,
John C. Mitchell:
ML and Beyond.
SIGPLAN Notices 32(1): 80-85 (1997) |
| 1996 |
| 30 | EE | David Tarditi,
J. Gregory Morrisett,
Perry Cheng,
Chris Stone,
Robert Harper,
Peter Lee:
TIL: a type-directed, optimizing compiler for ML (with retrospective)
Best of PLDI 1996: 554-567 |
| 29 | | David Tarditi,
J. Gregory Morrisett,
Perry Cheng,
Chris Stone,
Robert Harper,
Peter Lee:
TIL: A Type-Directed Optimizing Compiler for ML.
PLDI 1996: 181-192 |
| 28 | EE | Yasuhiko Minamide,
J. Gregory Morrisett,
Robert Harper:
Typed Closure Conversion.
POPL 1996: 271-283 |
| 27 | | Robert Harper,
Peter Lee:
Research in Programming Languages for Composability, Safety, and Performance.
ACM Comput. Surv. 28(4es): 195 (1996) |
| 26 | | Robert Harper,
John C. Mitchell:
ML and Beyond.
ACM Comput. Surv. 28(4es): 219 (1996) |
| 25 | EE | Robert Harper:
A Note on ``A Simplified Account of Polymorphic References''.
Inf. Process. Lett. 57(1): 15-16 (1996) |
| 24 | | Robert Harper,
Mark Lillibridge:
Operational Interpretations of an Extension of Fomega with Control Operators.
J. Funct. Program. 6(3): 393-417 (1996) |
| 1995 |
| 23 | | J. Gregory Morrisett,
Matthias Felleisen,
Robert Harper:
Abstract Models of Memory Management.
FPCA 1995: 66-77 |
| 22 | | Robert Harper,
J. Gregory Morrisett:
Compiling Polymorphism Using Intensional Type Analysis.
POPL 1995: 130-141 |
| 1994 |
| 21 | EE | 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 |
| 20 | | Robert Harper,
Mark Lillibridge:
A Type-Theoretic Approach to Higher-Order Modules with Sharing.
POPL 1994: 123-137 |
| 19 | | Robert Harper,
Donald Sannella,
Andrzej Tarlecki:
Structured Theory Presentations and Logic Representations.
Ann. Pure Appl. Logic 67(1-3): 113-160 (1994) |
| 18 | | Robert Harper:
A Simplified Account of Polymorphic References.
Inf. Process. Lett. 51(4): 201-206 (1994) |
| 1993 |
| 17 | | Robert Harper,
Mark Lillibridge:
Explicit Polymorphism and CPS Conversion.
POPL 1993: 206-219 |
| 16 | EE | Robert Harper,
John C. Mitchell:
On the Type Structure of Standard ML.
ACM Trans. Program. Lang. Syst. 15(2): 211-252 (1993) |
| 15 | EE | Robert Harper,
Furio Honsell,
Gordon D. Plotkin:
A Framework for Defining Logics.
J. ACM 40(1): 143-184 (1993) |
| 14 | | Robert Harper,
Bruce F. Duba,
David B. MacQueen:
Typing First-Class Continuations in ML.
J. Funct. Program. 3(4): 465-484 (1993) |
| 13 | | Robert Harper,
Mark Lillibridge:
Polymorphic Type Assignment and CPS Conversion.
Lisp and Symbolic Computation 6(3-4): 361-380 (1993) |
| 1992 |
| 12 | | Robert Harper:
Constructing Type Systems over an Operational Semantics.
J. Symb. Comput. 14(1): 71-84 (1992) |
| 1991 |
| 11 | | Robert Harper,
Benjamin C. Pierce:
A Record Calculus Based on Symmetric Concatenation.
POPL 1991: 131-142 |
| 10 | | Bruce F. Duba,
Robert Harper,
David B. MacQueen:
Typing First-Class Continuations in ML.
POPL 1991: 163-173 |
| 9 | | Robert Harper,
Robert Pollack:
Type Checking with Universes.
Theor. Comput. Sci. 89(1): 107-136 (1991) |
| 1990 |
| 8 | | Robert Harper,
John C. Mitchell,
Eugenio Moggi:
Higher-Order Modules and the Phase Distinction.
POPL 1990: 341-354 |
| 1989 |
| 7 | | Robert Harper,
Donald Sannella,
Andrzej Tarlecki:
Logic Representation in LF.
Category Theory and Computer Science 1989: 250-272 |
| 6 | | Robert Harper,
Donald Sannella,
Andrzej Tarlecki:
Structure and Representation in LF
LICS 1989: 226-237 |
| 5 | | Robert Harper,
Robert Pollack:
Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft).
TAPSOFT, Vol.2 1989: 241-256 |
| 1988 |
| 4 | | John C. Mitchell,
Robert Harper:
The Essence of ML.
POPL 1988: 28-46 |
| 1987 |
| 3 | | Robert Harper,
Furio Honsell,
Gordon D. Plotkin:
A Framework for Defining Logics
LICS 1987: 194-204 |
| 2 | | Robert Harper,
Robin Milner,
Mads Tofte:
A Type Discipline for Program Modules.
TAPSOFT, Vol.2 1987: 308-319 |
| 1985 |
| 1 | EE | Robert Harper:
Modules and Persistence in Standard ML.
Data Types and Persistence (Appin) 1985: 21-30 |