Pages that link to "Item:Q1961921"

The following pages link to Some lambda calculus and type theory formalized (Q1961921):

Displaying 35 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)
• Using typed lambda calculus to implement formal systems on a machine (Q688571) (← 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)
• Infinite \(\lambda\)-calculus and types (Q1275621) (← 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 \(\pi\)-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)
• (Q3138540) (← links)
• I Got Plenty o’ Nuttin’ (Q3188289) (← links)
• Generalizing Automath by means of a lambda-typed lambda calculus (Q3793765) (← links)
• Thunks and the λ-calculus (Q4358459) (← links)
• Important Issues in Foundational Formalisms (Q4842275) (← links)
• (Q4849246) (← links)
• (Q4856946) (← links)
• A PVS Theory for Term Rewriting Systems (Q5178962) (← links)
• Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
• Factorization and normalization, essentially (Q6536313) (← links)