Checking algorithms for Pure Type Systems

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

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

Abstract

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
PublisherSpringer
Pages19-61
Number of pages43
ISBN (Electronic)9783540484400
ISBN (Print)9783540580850
DOIs
Publication statusPublished - 1994

Publication series

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

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

  • Cite this

    Benthem Jutting, L. S., McKinna, J., & Pollack, R. (1994). Checking algorithms for Pure Type Systems. In Types for Proofs and Programs. TYPES 1993 (pp. 19-61). (Lecture Notes in Computer Science; Vol. 806). Springer. https://doi.org/10.1007/3-540-58085-9_71