Pages that link to "Item:Q1961921"
From MaRDI portal
The following pages link to Some lambda calculus and type theory formalized (Q1961921):
Displayed 26 items.
- Nominal lambda calculus: an internal language for FM-Cartesian closed categories (Q265798) (← links)
- Alpha equivalence equalities (Q428860) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
- Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
- Abstract abstract reduction (Q817587) (← links)
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations (Q853738) (← links)
- Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters (Q884953) (← links)
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
- Alpha-conversion and typability (Q1854262) (← links)
- Nominal logic, a first order theory of names and binding (Q1887151) (← links)
- The locally nameless representation (Q1945914) (← links)
- A solution to the PoplMark challenge based on de Bruijn indices (Q1945917) (← links)
- Mechanizing metatheory without typing contexts (Q2352491) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- A general mathematics of names (Q2373874) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations (Q2841231) (← links)
- The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) (Q2841232) (← links)
- The Theory of Contexts for First Order and Higher Order Abstract Syntax (Q2841274) (← links)
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming (Q2875221) (← links)
- I Got Plenty o’ Nuttin’ (Q3188289) (← links)
- A PVS Theory for Term Rewriting Systems (Q5178962) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)