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

A Universe of Binding and Computation. Daniel R. Licata and Robert Harper. Submitted, March, 2009.
Beyond Nested Parallelism: Tight Bounds on Work-Stealing Overheads for Parallel Futures. Daniel Spoonhower, Guy E. Blelloch, Robert Harper, and Phillip Gibbons. Submitted, February, 2009.
Positively Dependent Types. Daniel R. Licata and Robert Harper. PLPV 2009, Savannah, GA January 2009.
Focusing on Binding and Computation. Daniel R. Licata, Noam Zeilberger, and Robert Harper. LICS 2008, Pittsburgh June 2008
Space Profiling for Parallel Functional Programs. Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, and Robert Harper. ICFP, September, 2008.

Research Talks

Focusing on Binding and Computation. INRIA Rocquencourt and University of Paris, October, 2008.
Mechanizing Metatheory. INRIA Orsay, October, 2008.
Mechanizing Metatheory Using LF and Twelf. University of Oregon Summer School on Logic and Theorem Proving in Programming Languages, Eugene, OR, July, 2008.

Ph.D. Students

Avijit Kumar. Languages for Authenticated Mobile Computing.
Daniel K. Lee. Mechanizing Language Definitions.
Dan Licata. Dependent Type Refinements.
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.
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, 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: Fri Mar 6 14:50:49 EST 2009