The Fox Project
Programming Language Design

Contents	Recent Talks \| Recent Publications \| Software \| Collaborations \| Further Links
Elsewhere	Bibliography

The research of the project on programming language design is concerned with developing new language technology for building reliable and efficient software systems. Our work spans the spectrum of programming languages, from high-level languages such as Standard ML and Twelf, to very low-level languages such as Touchstone and Typed Assembly Language. The goal of our research is to extend the expressive power of languages to make it easier to write efficient, reliable programs and to make it easier to maintain and modify them.

Our research on programming languages is grounded in type theory, a unifying conceptual framework for studying language features and their properties. Types allow us to express safety properties of programs that are enforced by the language implementation. These properties include data representations, loop invariants, and interfaces between program components. The success of types as a powerful aide to programmers is, by now, widely recognized; all modern programming languages are based on static type systems. The goal of our research is to develop new type systems that better support practical programming.

Our current research on language design focuses on these main topics:

Module systems. Mechanisms to support the flexible construction of large software systems from reusable components.

Refinement types. Specification and verification of invariants on data structures that are maintained by a program.

Staged computation. Segregation of computation into stages to support run-time code generation and specialization.

Typed logic programming. Operational interpretation of types as formulas of a higher-order logic.

Low-level languages. Description of invariants governing registers, stacks, and branch points in programs.

Recent Talks

Verifying Program Invariants with Refinement Types.: Frank Pfenning.
Princeton and Yale Colloquium Talks, February 2001.
Abstract, Related paper (ICFP'00)
The Practice of Type Theory in Programming Languages.: Robert Harper.
Dagstuhl 10th Anniversary Symposium, Saarbruecken, Germany, August, 2000.
Typed Assembly Language: Type Theory for Machine Code.: Karl Crary.
PCC Workshop.
Santa Barbara, California, June 2000.

Recent Publications

A Type System for Higher-Order Modules.: Karl Crary, Robert Harper, and Derek Dreyer.
Submitted for publication to Twenty-Ninth Symposium on Principles of Programming Languages (POPL'02).
Adaptive Functional Programming.: Umut A. Acar, Guy E. Blelloch, and Robert Harper.
Submitted for publication to Twenty-Ninth Symposium on Principles of Programming Languages (POPL'02).
An Expressive, Scalable Type Theory for Certified Code.: Karl Crary and Joseph C. Vanderwaart.
Technical Report CMU-CS-01-113, May 2001.
Toward a Practical Type Theory for Recursive Modules.: Derek R. Dreyer, Robert Harper, and Karl Crary.
Technical Report CMU-CS-01-112, March, 2001.
A Language-Based Approach to Security.: Fred B. Scneider, Greg Morrisett, and Robert Harper.
Informatics: 10 Years Ahead, 10 Years Back. Conference on the Occasion of Dagstuhl's 10th Anniversary. Springer-Verlag Lecture Notes in Computer Science v. 2000.
On the Unusual Effectiveness of Logic in Computer Science: Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion Kolaitis, Moshe Vardi, and Victor Vianu.
Bullet of the Association for Symbolic Logic, 2001 (to appear).
Intersection Types and Computational Effects.: Rowan Davies and Frank Pfenning.
Proceedings of the International Conference on Functional Programming (ICFP 2000), Montreal, Canada, pages 198-208, September 2000.
Slides.
What is a Recursive Module?: Karl Crary, Robert Harper, and Sidd Puri.
SIGPLAN '99 Conference on Programming Language Design and Implementation, Atlanta, GA, June, 1999, pp 50--63.
Dependent types in practical programming.: Hongwei Xi and Frank Pfenning.
In A. Aiken, editor, Conference Record of the 26th Symposium on Principles of Programming Languages (POPL'99), pages 214-227. ACM Press, January 1999.