A Type Inference Algorithm And Transition Semantics For Polymorphic C.
Abstract
In an attempt to bring the ML-style type inference to the C programming language, Smith and Volpano developed a type system for a dialect of C, called PolyC SmV96a SmV95b. PolyC extends C with ML-style polymorphism and a limited form of higher-order function. Smith and Volpano proved a type soundness theorem that basically says that evaluation of a well-typed PolyC program cannot fail due to a type mismatch. The type soundness proof is based on an operational characterization of a special kind of semantic formulation called a natural semantics. This thesis presents an alternative semantic formulation, called a transition semantics, that could be used in place of the natural semantics to prove type soundness. The primary advantage of the transition semantics is that it eliminates the extra operational level, but the disadvantage is that it consists of many more evaluation rules than the natural semantics. Thus it is unclear whether it is a suitable alternative to the two-level approach of Smith and Volpano. Further, the thesis gives the first full type inference algorithm for the type system of PolyC. Despite implicit variable dereferencing found in PolyC, the algorithm turns out to be a rather straight-forward extension of Damas and Milner's algorithm W DaM82. The algorithm has been implemented as an attribute grammar in Grammatech's SSL and a complete source code listing is given in the Appendix.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1996
- Accession Number
- ADA318845
Entities
People
- Mustafa Oezgen
Organizations
- Naval Postgraduate School