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)
surveyconstructive type theorypure type systemslambda calculusformal mathematicsformal proofformal definitionsLEGO proof checkerstandardization for beta reduction
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items
Nominal lambda calculus: an internal language for FM-Cartesian closed categories ⋮ Formal metatheory of the lambda calculus using Stoughton's substitution ⋮ Nominal logic, a first order theory of names and binding ⋮ A general mathematics of names ⋮ Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations ⋮ I Got Plenty o’ Nuttin’ ⋮ A canonical locally named representation of binding ⋮ Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ A formalization of the Knuth-Bendix(-Huet) critical pair theorem ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. ⋮ The locally nameless representation ⋮ A solution to the PoplMark challenge based on de Bruijn indices ⋮ Alpha equivalence equalities ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus ⋮ External and internal syntax of the \(\lambda \)-calculus ⋮ A PVS Theory for Term Rewriting Systems ⋮ Viewing \({\lambda}\)-terms through maps ⋮ A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations ⋮ The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) ⋮ The Theory of Contexts for First Order and Higher Order Abstract Syntax ⋮ Alpha-conversion and typability ⋮ Mechanizing metatheory without typing contexts ⋮ Contextual equivalence for inductive definitions with binders in higher order typed functional programming ⋮ Abstract abstract reduction
Uses Software
