School of Computing

Well-going programs can be typed

Stefan Kahrs

In Martin Hofmann, editor, Typed Lambda Calculi and Applications, number 2701 in LNCS, pages 182-196. Springer, June 2003.

Abstract

Well-Going Programs Can Be Typed

Stefan Kahrs

Abstract: Our idiomatically objectionable title is a pun on Milner's ``well-typed programs do not go wrong'' --- because we provide a completeness result for type-checking rather than a soundness result.

We show that the well-behaved functions of untyped PCF are already expressible in typed PCF: any equivalence class of the partial logical equivalence generated from the flat natural numbers in the model given by PCF's operational semantics is inhabited by a well-typed term.

Download publication 247 kbytes (PostScript)

Bibtex Record

@inproceedings{1649,
author = {Stefan Kahrs},
title = {Well-Going Programs Can Be Typed},
month = {June},
year = {2003},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2003/1649},
    publication_type = {inproceedings},
    submission_id = {13979_1057659218},
    ISBN = {3-540-40332-9},
    booktitle = {Typed Lambda Calculi and Applications},
    editor = {Martin Hofmann},
    number = {2701},
    series = {LNCS},
    publisher = {Springer},
    ISSN = {0302-9743},
    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