Robert Harper's Home Page

Robert Harper
Computer Science Department	Phone	+1 (412) 268-3675
Carnegie Mellon University	EMail	`[email protected]`
	PGP	Public Key
5000 Forbes Avenue	Office	9207 Gates-Hillman Center
Pittsburgh, PA 15213-3890	Assistant	Ben Cook (4113 GHC, x8-5310)

ACM Research Highlight: Cache Efficient Functional Algorithms. Guy E. Blelloch and Robert Harper. Communications of the ACM, July, 2015.
λ-Calculus: The Other Turing Machine. Guy E. Blelloch and Robert Harper. July 2015. (CMU CSD Fiftieth Anniversary volume, September, 2015.)
Computational Higher Type Theory I: Abstract Cubical Realizability. Carlo Angiuli, Robert Harper, and Todd Wilson. April, 2016.
Computational Higher Type Theory II: Dependent Cubical Realizability. Carlo Angiuli and Robert Harper. October, 2016.
Computational Higher Dimensional Type Theory. Carlo Angiuli and Robert Harper and Todd Wilson. July, 2016. POPL, Paris, January 2017.
Parallel Functional Arrays. Ananya Kumar and Guy E. Blelloch and Robert Harper. POPL, Paris, January 2017.
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. Joseph Tassarotti and Ralf Jung and Robert Harper. ESOP, Uppsala, April, 2017.
Algorithmic λ-Calculus for the Design, Analysis, and Implementation of Parallel Algorithms. Umut Acar, Guy Blelloch, Robert Harper, and John Reppy. Research Project Proposal, October, 2016.
Meaning Explanations at Higher Dimension.Carlo Angiuli and Robert Harper. Brouwer Symposium submission, November 2016. Draft.

Computational Higher Type Theory. Gordon Plotkin 70th Birthday Celebration, Edinburgh, September, 2016.
Computational Higher Type Theory. Workshop on Categorical Logic and Univalent Foundations, July, 2016.
Two Notions of Beauty in Programming. John C. Mitchell 60th Birthday Celebration. May, 2016.
Two Kinds of Foundations. Edinburgh University LFCS 30th Anniversary Symposium. April, 2016.
Two Notions of Beauty in Programming. SIGPLAN Programming Languages Mentoring Workshop 2016, St. Petersburg, FL, January, 2016.
λ-Calculus: The Other Turing Machine. Carnegie Mellon University Computer Science Department 50th Anniversary Celebration, October 2015. (Joint with Guy E. Blelloch.)

Arbob Ahmad. An Epistemic Formulation of Information Flow Security.
Kuen-Bang Hou (Favonia). Higher-Dimensional Types in the Mechanization of Homotopy Theory.
Carlo Angiuli. Computational Higher Type Theory.
Joseph Tassarotti. Mechanized Proof for Concurrent Programs.
Evan Cavallo. Synthetic Cohomology in Homotopy Type Theory.
Stefan Muller. Semantics and implementation of reactive programs. (Jointly advised with Umut Acar.)
Danny Gratzer. Undergraduate research on semantics of effects. (Jointly advised with Karl Crary.)
Ananya Kumar. Undergraduate research on parallel data structures. (Jointly advised with Guy Blelloch.)

External Scientific Member, Max Planck Institute for Software Systems, Kaiserslautern and Saarbruecken, Germany
Umut Acar. Parallel Programming.
Steve Awodey. Higher type theory.
Nick Benton. Type refinements for compiler correctness.
Guy Blelloch. Parallelism, cost semantics, integrating algorithms and programming languages.
Karl Crary. Certifying compilers, logical frameworks, mechanized metatheory.
Ed Morehouse. Higher type theory.
Todd Wilson. Computational Higher Type Theory.

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. Working Draft, 2013.
Robert Harper. Practical Foundations for Programming Languages (Second Edition)

"Don't worry about people stealing your ideas. If your ideas are any good, you'll have to ram them down people's throats." -- Howard Aiken

Last modified: Mon Dec 19 12:18:40 EST 2016