© University of Kent - Contact | Feedback | Legal | FOI | Cookies
About the completeness of type systems
Stefan Kahrs
In Maarten de Rijke, editor, Observational Equivalence and Logical Equivalence, pages 182-196. ESSLLI, August 1996.Abstract
The original purpose of type systems for programming languages was to prevent certain forms of run-time errors, like using a number as a function. Some type systems go as far as guaranteeing the absence of run-time errors, e.g.\ the type system of Standard ML. One can call such a type system ``sound''.
This raises the question of the dual notion of completeness, i.e.\ is everything typable that does not have run-time errors? Or, to put it in another way: does the type system restrict the expressive power of the underlying implementation in an undesirable way?
To make this rather vague idea precise we define an abstract notion of ``type system'', together with general notions of soundness and completeness. We examine several type systems for these properties, for instance $\lambda^\tau$ and PCF are both complete, but for very different reasons.
Download publication 78 kbytesBibtex Record
@conference{564, author = {Stefan Kahrs}, title = {About the completeness of type systems}, month = {August}, year = {1996}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/1996/564}, booktitle = {Observational Equivalence and Logical Equivalence}, editor = {Maarten de Rijke}, organization = {ESSLLI}, refereed = {yes}, }