Dan Grossman
University of Washington

Quantified Types in a Safe C-Level Language


Designing a type-safe programming language with mutation, aliasing and quantified (i.e., universal and existential) types is an error-prone activity, but one still worth undertaking.  Although plenty of safe languages exist to serve as guidance (e.g., Standard ML, Typed Assembly Language, and Generic Java), we have encountered interesting differences in designing Cyclone, a safe C-like language.  In particular, C's distinction between "left expressions" and "right expressions" can actually simplify issues surrounding polymorphic references.  However, existential types and the address-of operator must be combined carefully to avoid an unsoundness that was not
previously known.

In this talk, I will describe quantified types in Cyclone, present a C-level formal semantics, explain why Cyclone's type system is sound, and investigate the heretofore undiscovered soundness issue involving existential types and aliasing.

This work is described in the following publications, available at http://www.cs.washington.edu/homes/djg/publications.html.

[1]    Quantified Types in an Imperative Language. Dan Grossman.  Revision submitted for journal publication,
        December 2004.
[2]    Existential Types for Imperative Languages.  Dan Grossman.  Eleventh European Symposium on Programming,
        volume 2305 of Lecture Notes in Computer Science, pages 21--35, Grenoble, France, April 2002.

Host:  Karl Crary
Appointments:  Margaret Weigand

Wednesday, January 26, 2005
3:30 p.m.
Wean Hall 8220

Principles of Programming Seminars