Journal of Computer Science and Technology

, Volume 12, Issue 6, pp 555–563 | Cite as

The expansion postponement in Pure Type Systems

  • Song Fangmin 
Regular Papers


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 words

Type theory pure type system reduction and expansion 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Barendregt H P. Introduction to generalized type systems.J. Functional Programming, 1991, 1(2): 124–154.Google Scholar
  2. [2]
    Pollack R. Typechecking in pure type systems. In1992 Workship on Types for Proofs and Programs, Baastad, Sweden, 1992, pp.271–288.Google Scholar
  3. [3]
    van Benthem Jutting L Set al. Checking Algorithms for Pure Type System. 1993.Google Scholar
  4. [4]
    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

Copyright information

© Science Press, Beijing China and Allerton Press Inc. 1997

Authors and Affiliations

  • Song Fangmin 
    • 1
  1. 1.Department of Computer Science and State Key Laboratory for Novel Software TechnologyNanjing UniversityNanjing

Personalised recommendations