Robert Harper's Home Page

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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

Research Interests

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

Research Projects

Higher-Dimensional Type Theory.
Prospero Project. Integrating Types and Verification.
Manifest Security Project. Manifest Security.

Research Papers

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.
Foundations and Applications of Higher-Dimensional Directed Type Theory. Robert Harper. Project description submitted for review, December, 2010.
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. Submitted, July, 2012.

Public Presentations

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.

Ph.D. Students

Arbob Ahmad. Modeling Information Flow Using Epistemic Logic.
Carlo Angiuli. Homotopy Type Theory.

Collaborators

External Scientific Member, Max Planck Institute for Software Systems, Kaiserslautern and Saarbruecken, Germany
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, 2012.

Conferences and Workshops

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

Journals

Editorial Board Member, Journal of Functional Programming.
Editor, Information and Computation.
Editor, Higher Order and Symbolic Computation.

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 Aug 23 01:03:15 CEST 2012