A type inference algorithm and transition semantics for polymorphic C
Rasmussen, Craig W.
MetadataShow full item record
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
Approved for public release; distribution is unlimited.
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 ...
Volpano, Dennis; Smith, Geoffrey (1997-06);A type system is given that eliminates two kinds of covert flows in an imperative programming language. The first kind arises from nontermination and the other from partial operations that can raise exceptions. The key ...
Mayer, Michael McClanahan (Monterey, California. Naval Postgraduate School, 1989-06);Current search algorithms and heuristics perform very poorly in the highly realistic scenario of a physical agent traversing an initially unknown search space. They do not attempt to minimize the amount of movement ...