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

• Prospero Project. Integrating Types and Specifications.
• Manifest Security Project. Manifest Security.

Research Papers

• A Universe of Binding and Computation. Daniel R. Licata and Robert Harper. To appear, ICFP 2009.
• Beyond Nested Parallelism: Tight Bounds on Work-Stealing Overheads for Parallel Futures. Daniel Spoonhower, Guy E. Blelloch, Robert Harper, and Phillip Gibbons. To appear, SPAA 2009.
• Positively Dependent Types. Daniel R. Licata and Robert Harper. PLPV 2009, Savannah, GA January 2009.
• Focusing on Binding and Computation. Daniel R. Licata, Noam Zeilberger, and Robert Harper. LICS 2008, Pittsburgh June 2008
• Space Profiling for Parallel Functional Programs. Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, and Robert Harper. ICFP, September, 2008.
• Mechanized Definition of Standard ML (Alpha Release). Karl Crary and Robert Harper. Summer, 2009.
• Distributed Programming with Distributed Authorization. Kumar Avijit and Anupam Datta and Robert Harper. To appear, TLDI 2010, Madrid.

Research Talks

• Focusing on Binding and Computation. INRIA Rocquencourt and University of Paris, October, 2008.
• Mechanizing Metatheory. INRIA Orsay, October, 2008.
• Mechanizing Metatheory Using LF and Twelf. University of Oregon Summer School on Logic and Theorem Proving in Programming Languages, Eugene, OR, July, 2008.

Ph.D. Students

• Avijit Kumar. Secure Mobile Computing.
• Daniel K. Lee. Mechanizing Language Definitions.
• Dan Licata. Focusing on Binding and Computation.

Collaborators

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

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: Mon Nov 16 13:36:00 EST 2009