Checking Algorithms for Pure Type Systems

L. S. van Benthem Jutting, James McKinna, Robert Pollack

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We have presented efficient syntax directed presentations of two subclasses of PTS:
— the semi-full systems, via the ⊢ sdsf relation
— the functional systems, via the ⊢f relation

The only remaining defect in these presentations lies in the possible failure of tests for conversion in the application rule. Thus for normalizing functional and semi-full systems, everything has been said.

For non-functional systems the situation is less clear. We know of no a priori bound on the amount of reduction necessary to correctly type λ-abstractions, so we must be content with the collective completeness of the family of syntax directed systems ⊢sd−n.

We have made little impact on the Expansion Postponement problem, which we leave as future work. We can however bask in the relative peace of mind gained from the machine-checked presentation of most (i.e. those not concerning schematic judgments) of the above results.
Original languageUndefined/Unknown
Title of host publicationTypes for Proofs and Programs
Subtitle of host publicationInternational Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers
EditorsHenk Barendregt, Tobias Nipkow
Place of PublicationBerlin
PublisherSpringer Berlin
Number of pages43
ISBN (Electronic)978-3-540-48440-0
ISBN (Print)978-3-540-58085-0
Publication statusE-pub ahead of print - 28 May 1993
EventTypes for Proofs and Programs: International Workshop TYPES'93 Nijmegen, The Netherlands, May 24–28, 1993 - Nijmegen, Netherlands
Duration: 24 May 199328 May 1993

Publication series

NameLecture Notes in Computer Science


ConferenceTypes for Proofs and Programs
Abbreviated titleTYPES 1993
Internet address


  • Induction Hypothesis
  • Side Condition
  • Schematic Term
  • Weak Closure
  • Small Relation

Cite this