Contact

All Stories

  1. Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory

    Article • Proceedings of the ACM on Programming Languages, January 2026, ACM (Association for Computing Machinery)

    Professor Robert Harper

  2. Mechanizing Synthetic Tait Computability in Istari

    Article • January 2026, ACM (Association for Computing Machinery)

    Professor Robert Harper

  3. Decalf: A Directed, Effectful Cost-Aware Logical Framework

    Article • Proceedings of the ACM on Programming Languages, January 2024, ACM (Association for Computing Machinery)

    Professor Robert Harper

  4. A cost-aware logical framework

    Article • Proceedings of the ACM on Programming Languages, January 2022, ACM (Association for Computing Machinery)

    Professor Robert Harper, Harrison Grodin

  5. Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

    Article • Journal of the ACM, December 2021, ACM (Association for Computing Machinery)

    Professor Robert Harper

  6. The history of Standard ML

    Article • Proceedings of the ACM on Programming Languages, June 2020, ACM (Association for Computing Machinery)

    Professor Robert Harper

  7. Higher inductive types in cubical computational type theory

    Article • Proceedings of the ACM on Programming Languages, January 2019, ACM (Association for Computing Machinery)

    Professor Robert Harper

  8. A separation logic for concurrent randomized programs

    Article • Proceedings of the ACM on Programming Languages, January 2019, ACM (Association for Computing Machinery)

    Professor Robert Harper

  9. Competitive parallelism: getting your priorities right

    Article • Proceedings of the ACM on Programming Languages, July 2018, ACM (Association for Computing Machinery)

    Professor Robert Harper

  10. Guarded Computational Type Theory

    Article • July 2018, ACM (Association for Computing Machinery)

    Professor Robert Harper

  11. Responsive parallel computation: bridging competitive and cooperative threading

    Article • ACM SIGPLAN Notices, September 2017, ACM (Association for Computing Machinery)

    Professor Robert Harper

  12. Parallel functional arrays

    Article • ACM SIGPLAN Notices, May 2017, ACM (Association for Computing Machinery)

    Professor Robert Harper

  13. Computational higher-dimensional type theory

    Article • ACM SIGPLAN Notices, May 2017, ACM (Association for Computing Machinery)

    Professor Robert Harper

  14. Parallel functional arrays

    Article • January 2017, ACM (Association for Computing Machinery)

    Professor Robert Harper

  15. Computational higher-dimensional type theory

    Article • January 2017, ACM (Association for Computing Machinery)

    Professor Robert Harper

  16. Cache efficient functional algorithms

    Article • Communications of the ACM, June 2015, ACM (Association for Computing Machinery)

    Professor Robert Harper

  17. Homotopical patch theory

    Article • ACM SIGPLAN Notices, November 2014, ACM (Association for Computing Machinery)

    Professor Robert Harper