Research Interests

• Type theory for programming language design and implementation.
• Logical frameworks and meta-languages.
• Algorithms and programming languages
• Trustless computation grids.
• Secure information grids.

Research Projects

• ConCert Project. Trustless Grid Computing.
• Triple Project. Type Refinement in Programming Languages.

Research Papers

• Focusing on Binding and Computation. Daniel R. Licata, Noam Zeilberger, and Robert Harper. February, 2008.
• Dependently Typed Programming With Domain-Specific Logics. Daniel R. Licata and Robert Harper. April, 2008.
• Space Profiling for Parallel Functional Programs. Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, and Robert Harper. April, 2008.

Research Talks

• Extensible Indexed Types. IFIP WG2.8 Working Group on Functional Programming, Iceland, July, 2007.
• Manifest Safety and Security. High-Confidence Software Systems 2007, Baltimore, MD, May, 2007.
• Mechanizing Language Definitions. University of Texas at Austin Distinguished Lecture Series, February, 2006.
• Mechanizing Language Definitions. Invited lecture, International Conference on Functional Programming (ICFP), Tallinn, September, 2005.
• Self-Adjusting Computation. Invited lecture, ICALP and LICS, Turku, Finland, July, 2004.
• Programming Languages: The Essence of Computer Science. University of Washington Distinguished Lecture Series, October, 2002.

Ph.D. Students

• Avijit Kumar. Languages for Authenticated Mobile Computing.
• Daniel K. Lee. Mechanizing Language Definitions.
• Dan Licata. Dependent Type Refinements.
• Tom Murphy. Modal Types for Mobile Code. (Co-advisor: Karl Crary).
• Dan Spoonhower. Parallel Real-time Programming Languages. (Co-advisor: Guy Blelloch).

Collaborators

• Guy Blelloch. Data parallel languages, adaptive computation.
• Karl Crary. Certifying compilers, programming language design.
• Peter Lee. Certifying compilers.
• Frank Pfenning. Logical frameworks, refinement types.
• David Walker. Refinement types for imperative programming.

Courses

• 15-212: Fundamental Principles of Programming.
• 15-312: Principles of Programming Languages.
• 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-399/15-317: Constructive Logic.
• 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.

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. Draft, 2005.
• Robert Harper. Practical Foundations for Programming Languages. Working draft, 2006.
• Robert Harper. Type Systems for Programming Languages. Draft, 2000.

Conferences and Workshops

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

Journals

• Editor (Programming Languages), Journal of the ACM.
• Editor, Higher Order and Symbolic Computation.

Personal

Last modified: Sat Apr 5 18:44:18 EDT 2008