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 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.

Research Papers

Mechanized Definition of Standard ML (Alpha Release). Karl Crary and Robert Harper. Summer, 2009.
A Universe of Binding and Computation. Daniel R. Licata and Robert Harper. ICFP, Edinburgh, September 2009.
Beyond Nested Parallelism: Tight Bounds on Work-Stealing Overheads for Parallel Futures. Daniel Spoonhower, Guy E. Blelloch, Robert Harper, and Phillip Gibbons. SPAA, September 2009.
Distributed Programming with Distributed Authorization. Kumar Avijit and Anupam Datta and Robert Harper. TLDI 2010, Madrid.
A Monadic Formalization of ML5 (Preliminary Version). Daniel R. Licata and Robert Harper. Submitted, April, 2010.

Public Presentations

Robin Milner 1934-2010. MFPS, Ottawa, May, 2010.
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

Arbob Ahmad. Secure Mashup Languages.
Dan Licata. Focusing on Binding and Computation.

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, 2008.

Conferences and Workshops

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

Journals

Editor (Programming Languages), Journal of the ACM.
Theoretical Pearls Editor, Journal of Functional Programming.
Editor, Information and Computation.
Editor, Higher Order and Symbolic Computation.

Personal

Last modified: Wed May 26 16:08:37 EDT 2010