×

Defining \(\lambda\)-typed \(\lambda\)-calculi by axiomatizing the typing relation. (English) Zbl 0797.68144

Enjalbert, Patrice (ed.) et al., STACS 93. 10th annual symposium on theoretical aspects of computer science, Würzburg, Germany, February 25-27, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 665, 712-723 (1993).
Summary: We present a uniform framework for defining different \(\lambda\)-typed \(\lambda\)-calculi in terms of systems to derive typing judgements, akin to Barendregt’s pure type systems. We first introduce a calculus called \(\lambda^ \lambda\) and study its abstract properties. These are, among others, the property of Church-Rosser, the property of subject reduction, and the one of strong normalization. Then we show how to extend \(\lambda^ \lambda\) to obtain an inferential definition of Nederpelt’s \(\Lambda\). One may also extend \(\lambda^ \lambda\) to get inferential definitions of van Daalen \(\Lambda_ \beta\), and de Bruijn’s \(\Lambda\Delta\) and we argue that these new inferential definitions are well suited for language-theoretic investigations.
For the entire collection see [Zbl 0866.00060].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B40 Combinatory logic and lambda calculus
68Q45 Formal languages and automata
PDFBibTeX XMLCite