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

Prospero Project. Integrating Types and Specifications.
Manifest Security Project. Manifest Security.
ConCert Project. Trustless Grid Computing.
Triple Project. Type Refinement in Programming Languages.

Research Papers

Focusing on Binding and Computation. Daniel R. Licata, Noam Zeilberger, and Robert Harper. February, 2008.
Dependently Typed Programming With Domain-Specific Logics. Daniel R. Licata and Robert Harper. July, 2008.
Space Profiling for Parallel Functional Programs. Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, and Robert Harper. April, 2008.

Research Talks

Extensible Indexed Types. IFIP WG2.8 Working Group on Functional Programming, Iceland, July, 2007.
Manifest Safety and Security. High-Confidence Software Systems 2007, Baltimore, MD, May, 2007.
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/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.

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. Draft, 2005.
Robert Harper. Practical Foundations for Programming Languages. Working Draft, 2008.

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: Wed Jul 16 15:01:08 EDT 2008