School of Computing

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 kbytes

Bibtex 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},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014