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

Authors

  • Milena Stefanova

Keywords:

inductive 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.

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://stipendii.uni-sofia.bg/index.php/fmi/article/view/284

Issue

Vol. 90 (1998): Ann. Sofia Univ. Fac. Math and Inf.

Section

Articles