Robert Harper's Home Page

Robert Harper
	Phone	+1 (412) 268-3675
Computer Science Department	Fax	+1 (412) 268-4801
Carnegie Mellon University	EMail	`rwh@cs.cmu.edu`
5000 Forbes Avenue	Office	9207 Gates-Hillman Center
Pittsburgh, PA 15213-3890	Assistant	Kathy McNiff

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

A Monadic Formalization of ML5 (Preliminary Version). Daniel R. Licata and Robert Harper. Logical Frameworks and Metalanguages: Theory and Practice (LFMTP), July, 2010.
Robin Milner 1934--2010: Verification, Languages, Concurrency. Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, and Peter Sewell. POPL 2011.
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 2013, Rome, Italy.
An Epistemic Formulation of Information Flow Analysis. Arbob Ahmad and Robert Harper. Submitted, February 2013.
Correctness of Compiling Polymorphism to Dynamic Typing". Kuen-Bang Hou (Favonia) and Robert Harper. Submitted, March, 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.

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.

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.

Last modified: Wed Apr 10 13:09:42 EDT 2013