Dan
Grossman
University
of
Washington
Quantified Types in a Safe C-Level
Language
Abstract:
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.
Principles
of Programming Seminars