Robert Harper - RankMe

166 papers A* 33A 11B 13Misc 1Journal 77Unranked 26

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory. Proc. ACM Program. Lang. Harrison Grodin, Runming Li, Robert Harper
2026	B	`conf`	Mechanizing Synthetic Tait Computability in Istari. CPP Runming Li, Yue Yao, Robert Harper
2026	—	`conf`	Recursive Logical Relations for Intuitionistic Linear Logic Session Types. ESOP (1) Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao
2025	J	`jnl`	Abstraction Functions as Types. CoRR Harrison Grodin, Runming Li, Robert Harper
2025	J	`jnl`	Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability. CoRR Runming Li, Robert Harper
2025	J	`jnl`	Mechanizing Synthetic Tait Computability in Istari. CoRR Runming Li, Yue Yao, Robert Harper
2024	B	`conf`	Amortized Analysis via Coalgebra. MFPS Harrison Grodin, Robert Harper
2024	B	`conf`	Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory. MFPS Yue Niu, Jonathan Sterling, Robert Harper
2024	J	`jnl`	Decalf: A Directed, Effectful Cost-Aware Logical Framework. Proc. ACM Program. Lang. Harrison Grodin, Yue Niu, Jonathan Sterling, Robert Harper
2023	A*	`conf`	A Metalanguage for Cost-Aware Denotational Semantics. LICS Yue Niu, Robert Harper
2023	J	`jnl`	A Verified Cost Analysis of Joinable Red-Black Trees. CoRR Runming Li, Harrison Grodin, Robert Harper
2023	B	`conf`	Amortized Analysis via Coinduction (Early Ideas). CALCO Harrison Grodin, Robert Harper
2023	J	`jnl`	Amortized Analysis via Coinduction. CoRR Harrison Grodin, Robert Harper
2023	J	`jnl`	Decalf: A Directed, Effectful Cost-Aware Logical Framework. CoRR Harrison Grodin, Robert Harper, Yue Niu, Jonathan Sterling
2023	B	`conf`	Integrating Cost and Behavior in Type Theory (Invited Talk). CALCO Robert Harper
2023	J	`jnl`	Logical Relations for Session-Typed Concurrency. CoRR Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao
2022	J	`jnl`	A cost-aware logical framework. Proc. ACM Program. Lang. Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper
2022	J	`jnl`	A metalanguage for cost-aware denotational semantics. CoRR Yue Niu, Robert Harper
2022	B	`conf`	Sheaf Semantics of Termination-Insensitive Noninterference. FSCD Jonathan Sterling, Robert Harper
2022	J	`jnl`	Sheaf semantics of termination-insensitive noninterference. CoRR Jonathan Sterling, Robert Harper
2021	J	`jnl`	A cost-aware logical framework. CoRR Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper
2021	J	`jnl`	An Equational Logical Framework for Type Theories. CoRR Robert Harper
2021	J	`jnl`	Internal Parametricity for Cubical Type Theory. Log. Methods Comput. Sci. Evan Cavallo, Robert Harper
2021	J	`jnl`	Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. J. ACM Jonathan Sterling, Robert Harper
2021	J	`jnl`	Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
2020	J	`jnl`	Cost-Aware Type Theory. CoRR Yue Niu, Robert Harper
2020	B	`conf`	Internal Parametricity for Cubical Type Theory. CSL Evan Cavallo, Robert Harper
2020	J	`jnl`	Internal Parametricity for Cubical Type Theory. CoRR Evan Cavallo, Robert Harper
2020	J	`jnl`	Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. CoRR Jonathan Sterling, Robert Harper
2020	J	`jnl`	The history of Standard ML. Proc. ACM Program. Lang. David MacQueen, Robert Harper, John H. Reppy
2019	J	`jnl`	A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. Joseph Tassarotti, Robert Harper
2019	J	`jnl`	Higher inductive types in cubical computational type theory. Proc. ACM Program. Lang. Evan Cavallo, Robert Harper
2019	J	`jnl`	Parametric Cubical Type Theory. CoRR Evan Cavallo, Robert Harper
2018	J	`jnl`	A Separation Logic for Concurrent Randomized Programs. CoRR Joseph Tassarotti, Robert Harper
2018	B	`conf`	Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. CSL Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper
2018	J	`jnl`	Competitive Parallelism: Getting Your Priorities Right. CoRR Stefan K. Muller, Umut A. Acar, Robert Harper
2018	J	`jnl`	Competitive parallelism: getting your priorities right. Proc. ACM Program. Lang. Stefan K. Muller, Umut A. Acar, Robert Harper
2018	J	`jnl`	Computational Higher Type Theory IV: Inductive Types. CoRR Evan Cavallo, Robert Harper
2018	J	`jnl`	Exception tracking in an open world. Theor. Comput. Sci. Robert Harper
2018	A*	`conf`	Guarded Computational Type Theory. LICS Jonathan Sterling, Robert Harper
2018	J	`jnl`	Guarded Computational Type Theory. CoRR Jonathan Sterling, Robert Harper
2018	—	`conf`	The RedPRL Proof Assistant (Invited Paper). LFMTP@FSCD Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, Jonathan Sterling
2018	B	`conf`	Verified Tail Bounds for Randomized Programs. ITP Joseph Tassarotti, Robert Harper
2017	A	`conf`	A Higher-Order Logic for Concurrent Termination-Preserving Refinement. ESOP Joseph Tassarotti, Ralf Jung, Robert Harper
2017	J	`jnl`	A Higher-Order Logic for Concurrent Termination-Preserving Refinement. CoRR Joseph Tassarotti, Ralf Jung, Robert Harper
2017	J	`jnl`	Algebraic Foundations of Proof Refinement. CoRR Jonathan Sterling, Robert Harper
2017	J	`jnl`	Computational Higher Type Theory III: Univalent Universes and Exact Equality. CoRR Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper
2017	A*	`conf`	Computational higher-dimensional type theory. POPL Carlo Angiuli, Robert Harper, Todd Wilson
2017	J	`jnl`	Correctness of compiling polymorphism to dynamic typing. J. Funct. Program. Kuen-Bang Hou (Favonia), Nick Benton, Robert Harper
2017	A*	`conf`	Parallel functional arrays. POPL Ananya Kumar, Guy E. Blelloch, Robert Harper
2017	A*	`conf`	Responsive parallel computation: bridging competitive and cooperative threading. PLDI Stefan K. Muller, Umut A. Acar, Robert Harper
2016	J	`jnl`	Computational Higher Type Theory I: Abstract Cubical Realizability. CoRR Carlo Angiuli, Robert Harper, Todd Wilson
2016	J	`jnl`	Computational Higher Type Theory II: Dependent Cubical Realizability. CoRR Carlo Angiuli, Robert Harper
2016	—	`conf`	Covering Spaces in Homotopy Type Theory. TYPES Kuen-Bang Hou (Favonia), Robert Harper
2016	J	`jnl`	Homotopical patch theory. J. Funct. Program. Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
2016	—	`book`	Practical Foundations for Programming Languages (2nd. Ed.). Robert Harper
2015	J	`jnl`	A Note on the Uniform Kan Condition in Nominal Cubical Sets. CoRR Robert Harper, Kuen-Bang Hou (Favonia)
2015	J	`jnl`	Cache efficient functional algorithms. Commun. ACM Guy E. Blelloch, Robert Harper
2015	J	`jnl`	Homotopy type theory: unified foundations of mathematics and computation. ACM SIGLOG News Steve Awodey, Robert Harper
2014	A	`conf`	Homotopical patch theory. ICFP Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
2013	A*	`conf`	Cache and I/O efficent functional algorithms. POPL Guy E. Blelloch, Robert Harper
2012	A*	`conf`	Canonicity for 2-dimensional type theory. POPL Daniel R. Licata, Robert Harper
2011	B	`conf`	2-Dimensional Directed Type Theory. MFPS Daniel R. Licata, Robert Harper
2011	A*	`conf`	Robin Milner 1934--2010: verification, languages, and concurrency. POPL Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell
2011	J	`jnl`	Selective Memoization CoRR Umut A. Acar, Guy E. Blelloch, Robert Harper
2010	—	`conf`	A Monadic Formalization of ML5 LFMTP Daniel R. Licata, Robert Harper
2010	—	`conf`	Distributed programming with distributed authorization. TLDI Kumar Avijit, Anupam Datta, Robert Harper
2010	J	`jnl`	Space profiling for parallel functional programs. J. Funct. Program. Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons
2009	—	`conf`	A Pronominal Approach to Binding and Computation. TLCA Robert Harper, Daniel R. Licata, Noam Zeilberger
2009	A	`conf`	A universe of binding and computation. ICFP Daniel R. Licata, Robert Harper
2009	J	`jnl`	An experimental analysis of self-adjusting computation. ACM Trans. Program. Lang. Syst. Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan
2009	J	`jnl`	An overview of the Oregon programming languages summer school. ACM SIGPLAN Notices 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
2009	B	`conf`	Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures. SPAA Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, Robert Harper
2009	J	`jnl`	FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum. J. Funct. Program. Robert Harper
2009	—	`conf`	Positively dependent types. PLPV Daniel R. Licata, Robert Harper
2009	A	`conf`	Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report. SIGCSE Mark W. Bailey, Kim B. Bruce, Kathleen Fisher, Robert Harper, Stuart Reges
2008	A*	`conf`	Focusing on Binding and Computation. LICS Daniel R. Licata, Noam Zeilberger, Robert Harper
2008	J	`jnl`	Position paper: practical foundations for lrogramming languages. ACM SIGPLAN Notices Robert Harper
2008	J	`jnl`	SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations. ACM SIGPLAN Notices 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
2008	A	`conf`	Space profiling for parallel functional programs. ICFP Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons
2007	J	`jnl`	Mechanizing metatheory in a logical framework. J. Funct. Program. Robert Harper, Daniel R. Licata
2007	A*	`conf`	Modular type classes. POPL Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller
2007	—	`conf`	Syntactic Logical Relations for Polymorphic and Recursive Types. Computation, Meaning, and Logic Karl Crary, Robert Harper
2007	A*	`conf`	Towards a mechanized metatheory of standard ML. POPL Daniel K. Lee, Karl Crary, Robert Harper
2007	—	`conf`	Type-Safe Distributed Programming with ML5. TGC Tom Murphy VII, Karl Crary, Robert Harper
2006	—	`conf`	A separate compilation extension to standard ML. ML David Swasey, Tom Murphy VII, Karl Crary, Robert Harper
2006	J	`jnl`	Adaptive functional programming. ACM Trans. Program. Lang. Syst. Umut A. Acar, Guy E. Blelloch, Robert Harper
2006	J	`jnl`	Extensional equivalence and singleton types. ACM Trans. Comput. Log. Christopher A. Stone, Robert Harper
2006	J	`jnl`	Higher-order abstract syntax: setting the record straight. SIGACT News Karl Crary, Robert Harper
2006	J	`jnl`	Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight CoRR Karl Crary, Robert Harper
2005	—	`conf`	A Library for Self-Adjusting Computation. ML Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan
2005	B	`conf`	Distributed Control Flow with Classical Modal Logic. CSL Tom Murphy VII, Karl Crary, Robert Harper
2005	A	`conf`	Mechanizing the meta-theory of programming languages. ICFP Robert Harper
2005	J	`jnl`	On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. Robert Harper, Frank Pfenning
2005	—	`conf`	Strict bidirectional type checking. TLDI Adam Chlipala, Leaf Petersen, Robert Harper
2005	B	`conf`	Using page residency to balance tradeoffs in tracing garbage collection. VEE Daniel Spoonhower, Guy E. Blelloch, Robert Harper
2004	A*	`conf`	A Symmetric Modal Lambda Calculus for Distributed Computing. LICS Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
2004	A*	`conf`	Dynamizing static algorithms, with applications to dynamic trees and history independence. SODA Umut A. Acar, Guy E. Blelloch, Robert Harper, Jorge L. Vittes, Shan Leung Maverick Woo
2004	J	`jnl`	Editorial. High. Order Symb. Comput. David A. Basin, Olivier Danvy, Robert Harper
2004	A*	`conf`	Self-Adjusting Computation. ICALP Robert Harper
2004	A*	`conf`	Self-Adjusting Computation. LICS Robert Harper
2004	—	`conf`	Self-adjusting beat detection and prediction in music. ICASSP (4) Robert Harper, M. Ed Jernigan
2003	A*	`conf`	A type system for higher-order modules. POPL Derek Dreyer, Karl Crary, Robert Harper
2003	A*	`conf`	A type theory for memory allocation and data layout. POPL Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
2003	A	`conf`	An effective theory of type refinements. ICFP Yitzhak Mandelbaum, David Walker, Robert Harper
2003	J	`jnl`	Automated techniques for provably safe mobile code. Theor. Comput. Sci. Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
2003	J	`jnl`	Automatic Generation of Staged Geometric Predicates. High. Order Symb. Comput. Aleksandar Nanevski, Guy E. Blelloch, Robert Harper
2003	A*	`conf`	Selective memoization. POPL Umut A. Acar, Guy E. Blelloch, Robert Harper
2003	—	`conf`	Typed compilation of recursive datatypes. TLDI Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
2002	A*	`conf`	Adaptive functional programming. POPL Umut A. Acar, Guy E. Blelloch, Robert Harper
2002	—	`conf`	Trustless Grid Computing in ConCert. GRID Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning
2001	A	`conf`	A Dependently Typed Assembly Language. ICFP Hongwei Xi, Robert Harper
2001	Misc	`conf`	A Language-Based Approach to Security. Informatics Fred B. Schneider, J. Gregory Morrisett, Robert Harper
2001	J	`jnl`	A Network Protocol Stack in Standard ML. High. Order Symb. Comput. Edoardo Biagioni, Robert Harper, Peter Lee
2001	A	`conf`	Automatic Generation of Staged Geometric Predicates. ICFP Aleksandar Nanevski, Guy E. Blelloch, Robert Harper
2001	J	`jnl`	On Equivalence and Canonical Forms in the LF Type Theory CoRR Robert Harper, Frank Pfenning
2001	J	`jnl`	On the unusual effectiveness of logic in computer science. Bull. Symb. Log. Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, Victor Vianu
2001	J	`jnl`	Persistent triangulations Journal of Functional Programming. J. Funct. Program. Guy E. Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary L. Miller, Noel Walkington
2001	—	`ed.`	Types in Compilation, Third International Workshop, TIC 2000, Montreal, Canada, September 21, 2000, Revised Selected Papers TIC Robert Harper
2000	—	`conf`	A type-theoretic interpretation of standard ML. Proof, Language, and Interaction Robert Harper, Christopher A. Stone
2000	A	`conf`	Advanced module systems: a guide for the perplexed (abstract of invited talk). ICFP Robert Harper, Benjamin C. Pierce
2000	A*	`conf`	Deciding Type Equivalence with Singleton Kinds. POPL Christopher A. Stone, Robert Harper
1999	J	`jnl`	Parametricity and Variants of Girard's Inf. Process. Lett. Robert Harper, John C. Mitchell
1999	J	`jnl`	Proof-Directed Debugging. J. Funct. Program. Robert Harper
1999	J	`jnl`	Relational Interpretations of Recursive Types in an Operational Setting. Inf. Comput. Lars Birkedal, Robert Harper
1999	A*	`conf`	What is a Recursive Module? PLDI Karl Crary, Robert Harper, Sidd Puri
1998	J	`jnl`	A Module System for a Programming Language Based on the LF Logical Framework. J. Log. Comput. Robert Harper, Frank Pfenning
1998	A*	`conf`	Generational Stack Collection and Profile-Driven Pretenuring. PLDI Perry Cheng, Robert Harper, Peter Lee
1998	—	`conf`	How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler. Types in Compilation Andrew Bernard, Robert Harper, Peter Lee
1997	J	`jnl`	ML and Beyond. ACM SIGPLAN Notices Robert Harper, John C. Mitchell
1997	—	`conf`	Relational Interpretations of Recursive Types in an operational Setting (Summary). TACS Lars Birkedal, Robert Harper
1997	—	`conf`	Typed Closure Conversion for Recursively-Defined Functions. HOOTS J. Gregory Morrisett, Robert Harper
1996	J	`jnl`	A Note on "A Simplified Account of Polymorphic References". Inf. Process. Lett. Robert Harper
1996	J	`jnl`	ML and Beyond. ACM Comput. Surv. Robert Harper, John C. Mitchell
1996	J	`jnl`	Operational Interpretations of an Extension of F J. Funct. Program. Robert Harper, Mark Lillibridge
1996	A	`ed.`	Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, Philadelphia, Pennsylvania, USA, May 24-26, 1996. ICFP Robert Harper, Richard L. Wexelblat
1996	J	`jnl`	Research in Programming Languages for Composability, Safety, and Performance. ACM Comput. Surv. Robert Harper, Peter Lee
1996	A*	`conf`	TIL: A Type-Directed Optimizing Compiler for ML. PLDI David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee
1996	—	`conf`	TIL: a type-directed, optimizing compiler for ML (with retrospective) Best of PLDI David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee
1996	A*	`conf`	Typed Closure Conversion. POPL Yasuhiko Minamide, J. Gregory Morrisett, Robert Harper
1995	—	`conf`	Abstract Models of Memory Management. FPCA J. Gregory Morrisett, Matthias Felleisen, Robert Harper
1995	A*	`conf`	Compiling Polymorphism Using Intensional Type Analysis. POPL Robert Harper, J. Gregory Morrisett
1994	J	`jnl`	A Simplified Account of Polymorphic References. Inf. Process. Lett. Robert Harper
1994	A*	`conf`	A Type-Theoretic Approach to Higher-Order Modules with Sharing. POPL Robert Harper, Mark Lillibridge
1994	—	`conf`	Signatures for a Network Protocol Stack: A Systems Application of Standard ML. LISP and Functional Programming Edoardo Biagioni, Robert Harper, Peter Lee, Brian Milnes
1994	J	`jnl`	Structured Theory Presentations and Logic Representations. Ann. Pure Appl. Log. Robert Harper, Donald Sannella, Andrzej Tarlecki
1993	J	`jnl`	A Framework for Defining Logics. J. ACM Robert Harper, Furio Honsell, Gordon D. Plotkin
1993	A*	`conf`	Explicit Polymorphism and CPS Conversion. POPL Robert Harper, Mark Lillibridge
1993	J	`jnl`	On the Type Structure of Standard ML. ACM Trans. Program. Lang. Syst. Robert Harper, John C. Mitchell
1993	J	`jnl`	Polymorphic Type Assignment and CPS Conversion. LISP Symb. Comput. Robert Harper, Mark Lillibridge
1993	J	`jnl`	Typing First-Class Continuations in ML. J. Funct. Program. Robert Harper, Bruce F. Duba, David B. MacQueen
1992	J	`jnl`	Constructing Type Systems over an Operational Semantics. J. Symb. Comput. Robert Harper
1991	A*	`conf`	A Record Calculus Based on Symmetric Concatenation. POPL Robert Harper, Benjamin C. Pierce
1991	J	`jnl`	Type Checking with Universes. Theor. Comput. Sci. Robert Harper, Robert Pollack
1991	A*	`conf`	Typing First-Class Continuations in ML. POPL Bruce F. Duba, Robert Harper, David B. MacQueen
1990	—	`book`	Definition of standard ML. Robin Milner, Mads Tofte, Robert Harper
1990	A*	`conf`	Higher-Order Modules and the Phase Distinction. POPL Robert Harper, John C. Mitchell, Eugenio Moggi
1989	—	`conf`	Logic Representation in LF. Category Theory and Computer Science Robert Harper, Donald Sannella, Andrzej Tarlecki
1989	A*	`conf`	Structure and Representation in LF LICS Robert Harper, Donald Sannella, Andrzej Tarlecki
1989	—	`conf`	Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft). TAPSOFT, Vol.2 Robert Harper, Robert Pollack
1988	A*	`conf`	The Essence of ML. POPL John C. Mitchell, Robert Harper
1987	A*	`conf`	A Framework for Defining Logics LICS Robert Harper, Furio Honsell, Gordon D. Plotkin
1987	—	`conf`	A Type Discipline for Program Modules. TAPSOFT, Vol.2 Robert Harper, Robin Milner, Mads Tofte
1986	—	`book`	Implementing mathematics with the Nuprl proof development system. 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
1985	—	`—`	Aspects of the Implementation of Type Theory. Robert Harper
1985	—	`conf`	Modules and Persistence in Standard ML. Data Types and Persistence (Appin) Robert Harper