The Triple Project
Type Refinement in Programming Languages

Research in the Triple project centers on the extension of syntactic type disciplines with a level of refinements that isolate properties of a type. Properties of interest include representation invariants on data structures, such as the coloring conditions on red/black trees, value range invariants, such as are required to support compile-time array bounds checking, and state invariants, which govern changes to mutable storage. Crucially, refinements are formally declared by the programmer, and rigorously checked by a mechanical refinement checker. This allows properties to be stated at module boundaries, and allows the programmer to ascertain that critical properties hold at specified points in a program.

We are developing a type-theoretic framework for type refinements that is general enough to capture both persistent and ephemeral properties of programs in the presence of effects. Persistent properties are those unchanged by effects, while ephemeral properties change with the program state.

We are also working on identifying practical sub-languages, balancing the expressive power of the refinement properties, the verbosity of the required refinement specifications, and the efficiency of automatic checking. For the latter, algorithms for program analysis, abstract interpretation, and model-checking will be critical tools. Our prior work on refinement types for data structure invariants and dependent types for static array bounds checking demonstrates that such a tradeoff can be made in a pragmatically successful way.

For additional detail, see the technical part of the project proposal from November 2001.

Researchers at Carnegie Mellon University

• Robert Harper, co-principal investigator
• Frank Pfenning, co-principal investigator
• Joshua Dunfield, graduate student
• Daniel Licata, graduate student
• Susmit Sarkar, graduate student

Collaborators

• Rowan Davies, University of Western Australia
• David Walker, Princeton University (the Plato project)
• Hongwei Xi, Boston University

Recent Drafts, Talks, and Publications

Tridirectional Typechecking

Joshua Dunfield and Frank Pfenning.
31st Annual Symposium on Principles of Programming Languages (POPL'04), Venice, Italy, January 2004.
To appear.

An Effective Theory of Type Refinements

Yitzhak Mandelbaum, David Walker, and Robert Harper.
Proceedings for the International Conference on Functional Programming (ICFP'03), Uppsala, Sweden, September 2003. To appear.
Extended version available as technical report, December 2002.
Extended PDF

Type Assignment for Intersections and Unions in Call-by-Value Languages

Joshua Dunfield and Frank Pfenning.
Proceedings of the 6th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'03), Warsaw, Poland.
A.D. Gordon, editor, pp 250-266, Springer-Verlag LNCS 2620, April 2003. © Springer-Verlag

Combining Two Forms of Type Refinements

Joshua Dunfield.
Technical Report CMU-CS-02-182, Carnegie Mellon University, September 2002.

Tri-Directional Type Checking

Frank Pfenning, joint work with Joshua Dunfield.
Workshop on Intersection Types and Related Systems (ITRS'02), July 2002.   Slides

Verifying Program Invariants with Refinement Types

Frank Pfenning.
Max-Planck-Institut Saarbrücken, October 2001.   Abstract   Slides
Princeton and Yale Colloquium Talks, February 2001.   Abstract   Slides

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

Support

The project is supported by the National Science Foundation under grant CCR-0204248: Type Refinements from September 1, 2002 until August 31, 2005.

[ Home | Publications | Software | Links ]

fp@cs.cmu.edu
http://www.cs.cmu.edu/~triple