A metalanguage for cost-aware denotational semantics. Yue Niu and Robert Harper. (Preprint.)
Jonathan Sterling and Robert Harper. FSCD 2022, August 2022.
A Cost-Aware Logical Framework.
Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. ACM PoPL Conference, January, 2022.
(Repository: Calf in Agda.)
Syntax and Models of Cartesian Cubical Type Theory.
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata.
Mathematical Structures in Computer Science, v.31, n.4, April 2021.
- A metalanguage for multi-phase modularity.
Jonathan Sterling and Robert Harper, ML Workshop 2021, August 2021.
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules.
Jonathan Sterling and Robert Harper. J. ACM v.68 n.6, October, 2021.
The History of Standard
ML. David MacQueen, Robert Harper, and John Reppy. ACM SIGPLAN History of Programming
Languages Conference IV, June 2020. (Presented, June 2021.)
Internal Parametricity for Cubical Type Theory,
Logical Methods in Computer Science, vol.17, no.4, November, 2021.
An Equational Logical Framework for Type
Theories. Robert Harper. arXiv 2106:01484, June, 2021.
Cost Semantics and Verification. Guy Blelloch's 60th Birthday Celebration, Pittsburgh, October 15, 2022.
Two Decades of OPLSS. Zena Ariola's 65th Birthday Celebration, ICFP, Ljubljana, September, 2022.
A (Logical) Framework for Collaboration. Frank Pfenning's 60th Birthday Celebration, Logical Frameworks, Metalanguages, and Theorem Proving (LFMTP 22), Haifa, August, 2022.
Formal (?) Education in PL at CMU. Workshop on Formal Education, Isaac Newton Institute, July 2022.
Phase Distinctions in Type Theory. Topos Institute, December, 2021.
Computational (Higher and Lower) Type Theory. MURI Meeting 2021, Pittsburgh, October 2021.
- Yue Niu. Cost-Aware Logical Frameworks. Proposal expected: Fall, 2022.
- Umut Acar. Parallel programming.
- Carlo Angiuli. Cubical Type
- Guy E. Blelloch.
Parallelism, cost semantics, integrating algorithms and programming languages.
- Evan Cavallo, University of Stockholm,
Sweden. Higher type theory.
- 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-21-0009, Tristan Nguyen,
Air Force Office of Scientific Research under award number FA9550-21-1-0385, Tristan Nguyen, program manager.
National Science Foundation grant CCF-1901381, "Algorithmic λ-Calculus for the Design, Analysis,
and Implementation of Parallel Algorithms."
Last modified: Tue Sep 28 22:08:06 EDT 2021