Recommendations
- Theorem Proving in Higher Order Logics
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- scientific article; zbMATH DE number 1414296
- scientific article; zbMATH DE number 1222556
- Induction-recursion and initial algebras.
- scientific article; zbMATH DE number 2079043
- scientific article; zbMATH DE number 3857082
- Towards an algebraic theory of recursion
- Structures for structural recursion
- Recursion-theoretic hierarchies
Cited in
(32)- Induction-recursion and initial algebras.
- A formalized general theory of syntax with bindings
- Binding operators for nominal sets
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- A formalized general theory of syntax with bindings: extended version
- Rensets and renaming-based recursion for syntax with bindings
- Mechanized metatheory revisited
- Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
- Formal metatheory of the lambda calculus using Stoughton's substitution
- Encoding abstract syntax without fresh names
- Formalizing adequacy: a case study for higher-order abstract syntax
- Nominal Lawvere theories: a category theoretic account of equational theories with names
- Normalization by evaluation and algebraic effects
- A simple nominal type theory
- Nominal equational logic
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming
- Foundations of nominal techniques: logic and semantics of variables in abstract syntax
- Structural recursion with locally scoped names
- A unified treatment of syntax with binders
- On Normalization by Evaluation for Object Calculi
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Formal SOS-Proofs for the Lambda-Calculus
- Abstract syntax: substitution and binders
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
- Theorem Proving in Higher Order Logics
- Denotational semantics with nominal Scott domains
- Rensets and renaming-based recursion for syntax with bindings extended version
- Nominal abstraction
- Nominal logic with equations only
- Nominal techniques in Isabelle/HOL
- External and internal syntax of the \(\lambda \)-calculus
This page was built for publication: Alpha-structural recursion and induction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3546313)
