Expansion Postponement for Normalising Pure Type Systems

Poll, Erik (1998) Expansion Postponement for Normalising Pure Type Systems. Journal of Functional Programming, 8 (1). pp. 89-96. ISSN 0956-7968. (doi:10.1017/s095679689700292x) (KAR id:21695)

PDF Language: English
Download this file (PDF/185kB)
Request a format suitable for use with assistive technology e.g. a screenreader
Postscript Language: English
Download this file (Postscript/143kB)	Preview
Request a format suitable for use with assistive technology e.g. a screenreader
Official URL: https://doi.org/10.1017/s095679689700292x

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.

Item Type:	Article
DOI/Identification number:	10.1017/s095679689700292x
Uncontrolled keywords:	Pure Type System, PTS
Subjects:	Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions:	Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User:	Mark Wheadon
Date Deposited:	31 Aug 2009 15:57 UTC
Last Modified:	09 Mar 2023 11:29 UTC
Resource URI:	https://kar.kent.ac.uk/id/eprint/21695 (The current URI for this page, for reference purposes)

University of Kent Author Information

Depositors only (login required):

Altmetric

Download Statistics

Total unique views for this document in KAR since July 2020. For more details click on the image.