School of Computing

Expansion Postponement for Normalising Pure Type Systems

Erik Poll

Journal of Functional Programming, 8(1):182-196, January 1998.

Abstract

Expansion Postponement is a tantalisingly simple conjecture about Pure Type Systems, which has so far resisted all attempts to prove it for any interesting class of systems. We prove the property for all normalising Pure Type Systems, and discuss the connection with typechecking.

Download publication 56 kbytes

Bibtex Record

@article{218,
author = {Erik Poll},
title = {{E}xpansion {P}ostponement for {N}ormalising {P}ure {T}ype {S}ystems},
month = {January},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/218},
    journal = {Journal of Functional Programming},
    number = {1},
    volume = {8},
}

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

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

Last Updated: 21/03/2014