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	7113 Wean Hall
Pittsburgh, PA 15213-3890	Secretary	Norene Mears

Research Interests

Programming languages: design, semantics, verification, and implementation.
Types in compilation: typed intermediate languages, type-based transformations, certifying compilers.
Logical frameworks and meta-languages.
Scientific computing.
Trustless grid computing.

Research Projects

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

Research Papers

Strict Bidirectional Type Checking. Adam Chlipala, Leaf Petersen, and Robert Harper. Types in Language Design and Implementation, 2005.
Distributed Control Flow with Classical Modal Logic. Tom Murphy VII, Karl Crary, and Robert Harper. Computer Science Logic: 19th Workshop, Oxford, UK, August, 2005.
Using Page Residency to Balance Tradeoffs in Tracing Garbage Collection. Daniel Spoonhower, Guy E. Blelloch, and Robert Harper. April, 2005. Virtual Execution Environments '05.
How To Believe a Twelf Proof. Robert Harper and Karl Crary. Unpublished manuscript, May, 2005.
Self-Adjusting Programming. Umut A. Acar, Guy E. Blelloch, Matthias Blume, and Robert Harper. To appear, ML Workshop '05, Tallinn, Estonia, September, 2005.
A Formulation of Dependent ML with Explicit Equality Proofs. Daniel R. Licata and Robert Harper. Carnegie Mellon University School of Computer Science Technical Report CMU-CS-05-178, December, 2005.
A Separate Compilation Extension to Standard ML. David Swasey, Tom Murphy VII, Karl Crary, and Robert Harper. Carnegie Mellon University School of Computer Science Technical Report CMU-CS-06-104, January, 2006.

Research Talks

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.
The Practice of Type Theory in Programming Languages. Dagstuhl 10th Anniversary Symposium. Saarbruecken, August, 2000.
Parallel Scientific Computing: The PSciCo Project at Carnegie Mellon. Edinburgh University, September, 2000.
Adaptive Functional Programming. University of New South Wales, May, 2002.
The ConCert Project. University of New South Wales, May, 2002.
Scottfest 2002: Types and Programming Languages. Carnegie Mellon University, October, 2002.
Programming Languages: The Essence of Computer Science. University of Washington Distinguished Lecture Series, October, 2002.

Ph.D. Students

Ashish Agarwal Modeling Theories and Optimization for Hybrid Systems (Co-advisor: Ignacio Grossmann)
Dan Licata. Dependent Type Refinements.
Tom Murphy. Type systems for mobile code. (Co-advisor: Karl Crary).
Dan Spoonhower. Parallel, real-time garbage collection. (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: 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.

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. Programming Languages: Theory and Practice. Draft, 2005.
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 Jan 28 18:29:55 EST 2006