Checking algorithms for Pure Type Systems

L. S. Benthem Jutting, J. McKinna, R. Pollack

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

22 Citations (Scopus)


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 languageEnglish
Title of host publicationTypes for Proofs and Programs. TYPES 1993
Number of pages43
ISBN (Electronic)9783540484400
ISBN (Print)9783540580850
Publication statusPublished - 1994

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Checking algorithms for Pure Type Systems'. Together they form a unique fingerprint.

Cite this