Quantified Types in a Safe C-Level
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
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
must be combined carefully to avoid an unsoundness that was not
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
Types in an Imperative Language. Dan Grossman. Revision submitted
for journal publication,
 Existential Types for Imperative Languages.
Dan Grossman. Eleventh European Symposium on Programming,
2305 of Lecture Notes in Computer
Science, pages 21--35, Grenoble, France, April 2002.
of Programming Seminars