Towards an ML-style polymorphic type system for C
Conference
Smith, G, Volpano, D. (1996). Towards an ML-style polymorphic type system for C
. Lecture Notes in Computer Science, 1058 341-355. 10.1007/3-540-61055-3_47
Smith, G, Volpano, D. (1996). Towards an ML-style polymorphic type system for C
. Lecture Notes in Computer Science, 1058 341-355. 10.1007/3-540-61055-3_47
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 pointer 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.
