Towards an ML-style Polymorphic Type System for C
MetadataShow full item record
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.
The article of record as published may be found at http://dx.doi.org/
Showing items related by title, author, creator and subject.
Smith, Geoffrey; Volpano, Dennis (1996);Advanced polymorphic type systems have come to play an important role in the world of functional programming. But, so far, these type systems have has little impact upon widely used imperative programming languages like ...
Bonem, Peter Bryant (Monterey, California. Naval Postgraduate School, 1995-09);Functional programming languages incorporate a number of powerful features, including advanced polymorphic type systems and first-class, higher- order functions. However, these important features have had little effect ...
Smith, Geoffrey; Volpano, Dennis (1996-05);In this article we consider the polymorphic type checking of an imperative language. Our lan- guage contains variables, first-class references (pointers), and first-class functions. Variables, as in traditional imperative ...