The expansion postponement in Pure Type Systems
The expansion postponement problem in Pure Type Systems is an open problem raised by R. Pollack in 1992. In this paper, the author presents a set of necessary and sufficient conditions for this problem and a set of sufficient conditions for it. The author also gives some properties for pure type systems without the expansion rule.
Key wordsType theory pure type system reduction and expansion
Unable to display preview. Download preview PDF.
- Barendregt H P. Introduction to generalized type systems.J. Functional Programming, 1991, 1(2): 124–154.Google Scholar
- Pollack R. Typechecking in pure type systems. In1992 Workship on Types for Proofs and Programs, Baastad, Sweden, 1992, pp.271–288.Google Scholar
- van Benthem Jutting L Set al. Checking Algorithms for Pure Type System. 1993.Google Scholar
- Barendregt H P. Lambda calculi with types. InHandbook of Logic in Computer Science, Vol II, Gabbai Abramsky, Maibaum (eds.), Oxford University Press, 1992.Google Scholar