### Abstract

We have presented efficient syntax directed presentations of two subclasses of PTS:

the semi-full systems, via the ⊢

the functional systems, via the ⊢

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 ⊢

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.

the semi-full systems, via the ⊢

_{sdsf}relationthe functional systems, via the ⊢

_{f}relationThe 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 language | English |
---|---|

Title of host publication | Types for Proofs and Programs. TYPES 1993 |

Publisher | Springer |

Pages | 19-61 |

Number of pages | 43 |

ISBN (Electronic) | 9783540484400 |

ISBN (Print) | 9783540580850 |

DOIs | |

Publication status | Published - 1994 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Volume | 806 |

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