Research Interests

• Principles of programming.

Papers

• Higher Inductive Types in Cubical Computational Type Theory. Evan Cavallo and Robert Harper. ACM Symposium on Principles of Programming Languages (PoPL), Lisbon, Portugal, January 2019.
• Internal Parametricity for Cubical Type Theory. Evan Cavallo and Robert Harper. To appear, Computer Science Logic, Barcelona, January, 2020.
• How to (Re)Invent Tait's Method. Robert Harper, July 2019.
• How to (Re)Invent Girard's Method. Robert Harper, July 2019.

Talks

• Three Varieties of Cubes in Computational Higher Type Theory. Eastern Great Lakes Programming Languages Symposium, Ithaca, May 10, 2019.
• Operational Semantics in Languages and Logics. Felleisen Halftime Celebration, Boston, November 2018.
• Computational Higher Type Theory (CHiTT). MURI Meeting 2018, Pittsburgh, March 2018.

Students

• Evan Cavallo. Higher Inductive Types and Parametricity in Cubical Type Theory. Expected: Summer, 2020. (M.Sc. Thesis: Synthetic Cohomology in Homotopy Type Theory. December, 2015.)
• Jonathan Sterling. Proof Assistants for Cubical Type Theory; Syntax and Semantics of Type Theory.
• Yue Niu. Dependent type theory for complexity analysis.

Collaborators

• Umut Acar. Parallel programming.
• Carlo Angiuli. Computational Cubical Type Theory.
• 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 type theory.
• 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.

Books

• Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
  (Available at SML Family Web Site.)
• Robert Harper (editor). Types in Compilation. Springer-Verlag Lecture Notes in Computer Science volume , 2001.
• Robert Harper. Programming in Standard ML. Draft, 2013.
• Robert Harper. Practical Foundations for Programming Languages (Second Edition)

Courses

• 15-150: Functional Programming.
• 15-210: Parallel and Sequential Data Structures and Algorithms.
• 15-312: Principles of Programming Languages.
• 15-317: Constructive Logic.
• 15-814: Types and Programming Languages.
• 15-819: Homotopy Type Theory.
• 15-819: Computational Higher Type Theory.
• Oregon Programming Languages Summer School 2017, 2016, 2015, 2014, 2013, 2012, 2011.
  (And all prior instances back to the first instance in 2002.)

Conferences and Workshops

• TYPES 2020. March 2-6 2020, Turin, Italy.
• FSCD 2020. June 29 - July 5, 2020, Paris.
• IFIP WG2.8 Working Group on Functional Programming.

Journals

• Editorial Board, Foundations and Trends in Programming Languages.

Web Sites

• SML Family. Standard ML family of languages.
• Homotopy Type Theory. Higher Type Theory blog.
• Twelf. Twelf Implementation of the LF Logical Framework.

Research Funding

• Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053, Tristan Nguyen, program manager.
• Air Force Office of Scientific Research under award number FA9550-19-1-0216, Tristan Nguyen, program manager.
• National Science Foundation grant CCF-1901381, "Algorithmic λ-Calculus for the Design, Analysis, and Implementation of Parallel Algorithms."

Last modified: Thu Oct 31 19:24:40 EDT 2019