- Principles of programming.
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules.
Jonathan Sterling and Robert Harper. Revised, October, 2020.
"The committee appreciated that the results are significant, relevant, and novel. In fact, so
novel that the paper may be one of the first of its kind, applying modern categorical type theory and homotopy type
theory to core programming languages questions. Unfortunately, the committee ultimately decided to accept other
excellent and more accessible papers ahead of this submission." -- PoPL 2020 PC
The History of Standard
ML. David MacQueen, Robert Harper, and John Reppy. To appear, ACM History of Programming
Languages Conference, 2021?
- Internal Parametricity for Cubical Type Theory. Evan Cavallo
and Robert Harper. Computer Science Logic, Barcelona, January, 2020. Revised and expanded, May 2020.
- Reynolds's Parametricity Theorem, Directly.
Robert Harper. Manuscript, March, 2020.
- A Semantic Logical Framework. Robert Harper. Manuscript, Spring, 2020.
- Mechanization of Type Safety of Standard ML. Karl Crary
and Robert Harper. August 15, 2009.
- Umut Acar. Parallel programming.
- Carlo Angiuli. Computational Cubical Type
- Guy E. Blelloch.
Parallelism, cost semantics, integrating algorithms and programming languages.
- Karl Crary.
Certifying compilers, logical frameworks, mechanized metatheory.
- Kuen-Bang Hou (Favonia), University of
Minnesota. Cubical computational type theory.
- Daniel R. Licata, Wesleyan University. Higher
- Anders Mörtberg, University of
Stockholm, Sweden. Higher type theory.
- Todd Wilson,
California State University Fresno. Cubical computational type theory.
- Max Planck
Institute for Software Systems, Kaiserslautern and Saarbruecken, Germany. External Scientific Member.
Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053, Tristan Nguyen,
Air Force Office of Scientific Research under award number FA9550-19-1-0216, Tristan Nguyen,
National Science Foundation grant CCF-1901381, "Algorithmic λ-Calculus for the Design, Analysis,
and Implementation of Parallel Algorithms."
Last modified: Tue Oct 20 10:47:10 EDT 2020