Pages that link to "Item:Q5917605"

The following pages link to Parallel reductions in \(\lambda\)-calculus (Q5917605):

Displaying 50 items.

• Compositional Z: confluence proofs for permutative conversion (Q514511) (← links)
• Abstract abstract reduction (Q817587) (← links)
• Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters (Q884953) (← links)
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
• Nominal techniques in Isabelle/HOL (Q928672) (← links)
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
• On the confluence of lambda-calculus with conditional rewriting (Q987976) (← links)
• The lambda-context calculus (extended version) (Q1044184) (← links)
• Needed reduction and spine strategies for the lambda calculus (Q1097253) (← links)
• A lambda-calculus for dynamic binding (Q1127514) (← links)
• Perpetual reductions in \(\lambda\)-calculus (Q1286373) (← links)
• Lambda-calculi for (strict) parallel functions (Q1314269) (← links)
• \(\lambda_{\beta'}\) -- a \(\lambda\)-calculus with a generalized \(\beta\)-reduction rule (Q1349744) (← links)
• A domain-theoretic semantics of lax generic functions. (Q1398469) (← links)
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
• Typed operational semantics for higher-order subtyping. (Q1401950) (← links)
• The Church-Rosser theorem and quantitative analysis of witnesses (Q1627965) (← links)
• Non-strictly positive fixed points for classical natural deduction (Q1772778) (← links)
• A proof of the leftmost reduction theorem for \(\lambda\beta\eta\)-calculus (Q1786610) (← links)
• Sequential evaluation strategies for parallel-or and related reduction systems (Q1825644) (← links)
• Descendants and origins in term rewriting. (Q1854348) (← links)
• Conservation and uniform normalization in lambda calculi with erasing reductions (Q1854562) (← links)
• Church-Rosser property of a simple reduction for full first-order classical natural deduction (Q1861541) (← links)
• A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
• A formal system of reduction paths for parallel reduction (Q1989338) (← links)
• A simplified proof of the Church-Rosser theorem (Q2016071) (← links)
• Decomposing probabilistic lambda calculi (Q2200818) (← links)
• The untyped computational \(\lambda \)-calculus and its intersection type discipline (Q2210507) (← links)
• Factorization in call-by-name and call-by-value calculi via linear logic (Q2233405) (← links)
• Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory (Q2333314) (← links)
• Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
• Confluence of orthogonal term rewriting systems in the prototype verification system (Q2362205) (← links)
• Strong normalization of classical natural deduction with disjunctions (Q2482841) (← links)
• Parallel reduction in type free lambda/mu-calculus (Q2703743) (← links)
• Toward a reduction system commuting with beta reduction in the partial lambda calculus (Q2768241) (← links)
• The mechanisation of Barendregt-style equational proofs (the residual perspective) (Q2841232) (← links)
• Term collections in {\(\lambda\)} and {\(\rho\)}-calculi (Q2864209) (← links)
• Distributive \(\rho\)-calculus (Q2873778) (← links)
• Amortized Complexity Verified (Q2945642) (← links)
• (Q2985126) (← links)
• I Got Plenty o’ Nuttin’ (Q3188289) (← links)
• Upper bounds for standardizations and an application (Q4254636) (← links)
• 1999–2000 Winter Meeting of the Association for Symbolic Logic (Q4508284) (← links)
• (Q4521592) (← links)
• More Church-Rosser proofs (in Isabelle/HOL) (Q4647561) (← links)
• Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060) (← links)
• From Search to Computation: Redundancy Criteria and Simplification at Work (Q4916077) (← links)
• Tactics and Parameters (Q4924546) (← links)
• Monotone (co)inductive types and positive fixed-point types (Q4943545) (← links)
• (Q5013828) (← links)