A SCHEMATIC PROOF OF STRONG NORMALIZATION FOR THE SYSTEMS OF THE $\lambda$-CUBE*

TitleA SCHEMATIC PROOF OF STRONG NORMALIZATION FOR THE SYSTEMS OF THE $\lambda$-CUBE*
Publication TypeJournal Article
Year of Publication1998
AuthorsStefanova M
JournalAnnuaire de l’Université de Sofia “St. Kliment Ohridski”. Faculté de Mathématiques et Informatique
Volume90
IssueLivre 1 - Mathématiques et Mecanique
Pagination17-40
ISSN0205-0808
Keywordsinductive types, normalization, typed lambda calculus
Abstract

This paper describes a set-theoretical argument for proving Strong Normalization (SN) for the systems of the so-called $\lambda$-cube. The argument is relatively simple and, moreover, flexible. It can be adapted to extensions of the systems considered, such as additional sorts, inductive types or sub-types.

1991/95 MSC

03B15, 03B40

AttachmentSize
PDF icon 90-017-040.pdf1.97 MB

© Faculty of Mathematics and Informatics