Skip to main content

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.

Download (265kB) Preview
Download (143kB) Preview


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
Uncontrolled keywords: Pure Type System, PTS
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 31 Aug 2009 15:57 UTC
Last Modified: 28 May 2019 14:01 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year