Towards an ML-style Polymorphic Type System for C

Advanced polymorphic type systems have come to play an important role in the world of functional programming. But, curiously, these type systems have so far had little impact upon widely-used imperative programming languages like C and C. We show that ML-style polymorphism can be integrated smoothly into a dialect of C, which we call Polymorphic C. It has the same point operations as C, including the address-of operator , the dereferencing operator , and pointer arithmetic. Our type system allows these operations in their full generality, so that programmers need not give up the flexibility of C to gain the benefits of ML-style polymorphism. We prove a type soundness theorem that gives a rigorous and useful characterization of well-typed Polymorphic C programs in terms of what can go wrong when they are evaluated.