Proofs of the normalization and Church-Rosser theorems for the typed \(\lambda\)-calculus
From MaRDI portal
Publication:1235139
DOI10.1305/ndjfl/1093888405zbMath0351.02019OpenAlexW2005924676MaRDI QIDQ1235139
Publication date: 1978
Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1305/ndjfl/1093888405
Related Items (2)
Higher-order unification with dependent function types ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
This page was built for publication: Proofs of the normalization and Church-Rosser theorems for the typed \(\lambda\)-calculus