Research Interests

• Type theory, proof theory, and category theory applied to programming language semantics and implementation.

Research Projects

• Homotopy Type Theory.
• Secure Composition of Systems and Policies.

Research Papers

• 2-Dimensional Directed Type Theory. Daniel R. Licata and Robert Harper. Mathematical Foundations of Program Semantics (MFPS), Pittsburgh, May, 2011.
• Canonicity for 2-Dimensional Type Theory. Daniel R. Licata and Robert Harper. POPL, Philadelphia, January 2012.
• Cache and I/O Efficient Functional Algorithms. Guy E. Blelloch and Robert Harper. POPL, Rome, Italy, January 2013.
• An Epistemic Formulation of Information Flow Security. Arbob Ahmad and Robert Harper. Submitted for publication, July, 2013.
• Type Refinements for Compiler Correctness. Kuen-Bang Hou (Favonia) and Robert Harper. Submitted for publication, July 2013.

Public Presentations

• Two Notions of Beauty in Programming. LICS/MFPS Joint Session in honor of Dana Scott, New Orleans, June, 2013.
• Functional IO Algorithms. POPL, Rome, Italy, January, 2013.
• Cache Efficient Functional Algorithms. Max Planck Institute for Informatics and for Software Systems, Saarbr\"{u}cken, Germany, August, 2012.
• Modules Matter Most. MacQueen Fest, Chicago, May, 2012.
• Defining a Language. Symposium in Honor of Robin Milner, Edinburgh, March, 2012.
• Robin Milner 1934-2010. POPL, Austin, TX, January, 2011.
• Robin Milner 1934-2010. MFPS, Ottawa, May, 2010.

Ph.D. Students

• Arbob Ahmad. Modeling Information Flow Using Epistemic Logic.
• Carlo Angiuli. Homotopy Type Theory.
• Kuen-Bang Hou (Favonia). Social Network Logic, Homotopy Type Theory.

Collaborators

• External Scientific Member, Max Planck Institute for Software Systems, Kaiserslautern and Saarbruecken, Germany
• Jeremy Avigad. Homotopy Type Theory.
• Steve Awodey. Homotopy Type Theory.
• Guy Blelloch. Data parallel languages, adaptive computation.
• Karl Crary. Certifying compilers, programming language design.
• Anupam Datta. Logics and languages for security.
• Frank Pfenning. Logical frameworks, refinement types.

Courses

• 15-312: Principles of Programming Languages.
• 15-150: Functional Programming.
• 15-317: Constructive Logic.
• 15-814: Type Systems for Programming Languages.
• 15-819: Advanced Topics in Programming Languages: Languages for Mobile Computing.
• 15-819: Advanced Topics in Programming Languages: Type Systems for Modularity.
• 15-819: Advanced Topics in Programming Languages: Type Refinements for Programming Languages.
• Types Systems as a Foundation for Reliable Computing, Summer School on Reliable Computing, Eugene, OR, July, 2005.
• 15-819: Advanced Topics in Programming Languages: Languages and Logics for Security.
• 15-819: Advanced Topics in Programming Languages: Theoretical Foundations for Programming Languages.

Books

• Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
• Robert Harper (editor). Types in Compilation. Springer-Verlag Lecture Notes in Computer Science volume , 2001.
• Robert Harper. Programming in Standard ML. Working Draft, 2013.
• Robert Harper. Practical Foundations for Programming Languages (Draft Copy).
  Hardcopy available from Cambridge University Press at 20% discount.
• The Univalent Foundations Program of the Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.

Conferences and Workshops

• Member, IFIP WG2.8 Working Group on Functional Programming.

Journals

• Editorial Board, Journal of Functional Programming.
• Editor, Higher Order and Symbolic Computation.
• Editorial Board, Foundations and Trends in Programming Languages.

Web Sites

• Existential Type. Research and teaching blog.
• Homotopy Type Theory. Higher-dimensional type theory blog.
• Twelf. Twelf system.
• Standard ML. Standard ML language and implementation.

Last modified: Thu Jul 11 15:49:52 EDT 2013