A SCHEMATIC PROOF OF STRONG NORMALIZATION FOR THE SYSTEMS OF THE $\lambda$-CUBE*
Keywords:
inductive types, normalization, typed lambda calculusAbstract
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.
Downloads
Published
1998-12-12
How to Cite
Stefanova, M. (1998). A SCHEMATIC PROOF OF STRONG NORMALIZATION FOR THE SYSTEMS OF THE $\lambda$-CUBE*. Ann. Sofia Univ. Fac. Math. And Inf., 90, 17–40. Retrieved from https://ftl5.uni-sofia.bg/index.php/fmi/article/view/284
Issue
Section
Articles