A sequent calculus formulation of type assignment with equality rules for the λβ-calculus

DOI10.2307/2273503zbMath0395.03014OpenAlexW1489404987MaRDI QIDQ4177542

Jonathan P. Seldin

Publication date: 1978

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2273503

zbMATH Keywords

Lambda-Beta CalculusNatural DeductionCut EliminationSequent CalculusType Assignment

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (1)

On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory

Cites Work

• Combinatory logic. Vol. II
• A sequent calculus for type assignment

This page was built for publication: A sequent calculus formulation of type assignment with equality rules for the λβ-calculus