Some lambda calculus and type theory formalized
From MaRDI portal
Publication:1961921
DOI10.1023/A:1006294005493zbMath0940.03019MaRDI QIDQ1961921
Publication date: 30 January 2000
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
survey; constructive type theory; pure type systems; lambda calculus; formal mathematics; formal proof; formal definitions; LEGO proof checker; standardization for beta reduction
Related Items
A formalization of the Knuth-Bendix(-Huet) critical pair theorem, Abstract abstract reduction, Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations, Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters, External and internal syntax of the \(\lambda \)-calculus, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Alpha-conversion and typability, Nominal logic, a first order theory of names and binding, A general mathematics of names
Uses Software