Pages that link to "Item:Q3546313"
From MaRDI portal
The following pages link to Alpha-structural recursion and induction (Q3546313):
Displaying 31 items.
- Normalization by evaluation and algebraic effects (Q265792) (← 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)
- Nominal abstraction (Q617715) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← links)
- Binding operators for nominal sets (Q1744371) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- Mechanized metatheory revisited (Q2323447) (← 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)
- Encoding abstract syntax without fresh names (Q2392477) (← links)
- Formalizing adequacy: a case study for higher-order abstract syntax (Q2392483) (← links)
- Nominal Lawvere theories: a category theoretic account of equational theories with names (Q2453579) (← links)
- A simple nominal type theory (Q2804939) (← links)
- Nominal equational logic (Q2864152) (← links)
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming (Q2875221) (← links)
- Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax (Q3011103) (← links)
- Structural recursion with locally scoped names (Q3016213) (← links)
- A unified treatment of syntax with binders (Q3165528) (← links)
- On Normalization by Evaluation for Object Calculi (Q3499758) (← links)
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention (Q5022932) (← links)
- Formal SOS-Proofs for the Lambda-Calculus (Q5178966) (← links)
- Abstract Syntax: Substitution and Binders (Q5262926) (← links)
- Theorem Proving in Higher Order Logics (Q5477644) (← links)
- Denotational Semantics with Nominal Scott Domains (Q5501931) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)