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	Assistant	April Foster

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

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

Research Papers

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.
Modular Type Classes. Derek Dreyer, Robert Harper, Manuel Chakravarti, and Gabriele Keller. ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007.
ALADDIN NextGen: Multiscale Scheduling, Integrating Parallel and Distributed Computation, Theory and Practice. G. E. Blelloch, L. Blum, M. Harchol-Balter, R. Harper, and R. Schwartz. May, 2006.
A Separate Compilation Extension to Standard ML. David Swasey, Tom Murphy VII, Karl Crary, and Robert Harper. 2006 ACM SIGPLAN Workshop on ML, Portland, OR, September, 2006.
Towards a Mechanized Metatheory for Standard ML. Daniel K. Lee, Karl Crary, and Robert Harper. ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007.
Syntactic Logical Relations for Polymorphic and Recursive Types. Karl Crary and Robert Harper. Manuscript, August 2006.
The Cult of the Bound Variable: The 9th Annual ICFP Programming Contest. Tom Murphy VII, Daniel Spoonhower, Chris Casinghino, Daniel R. Licata, Karl Crary and Robert Harper. September, 2006.
Mechanizing Metatheory in a Logical Framework. Robert Harper and Daniel Licata. To appear, Journal of Functional Programming. Draft of October, 2006.
Manifest Security. Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, and Stephan Zdancewic. January, 2007.

Research Talks

Mechanizing Language Definitions. University of Texas at Austin Distinguished Lecture Series, February, 2006.
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.
Programming Languages: The Essence of Computer Science. University of Washington Distinguished Lecture Series, October, 2002.

Ph.D. Students

Avijit Kumar. Languages for Authenticated Mobile Computing.
Daniel K. Lee. Mechanizing Language Definitions.
Dan Licata. Dependent Type Refinements.
Tom Murphy. Modal Types for Mobile Code. (Co-advisor: Karl Crary).
Dan Spoonhower. Parallel Real-time Programming Languages. (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. Practical Foundations for Programming Languages. Working draft, 2006.
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: Fri Jan 26 14:42:39 EST 2007