Alpha-structural recursion and induction
DOI10.1145/1147954.1147961zbMATH Open1326.68180OpenAlexW1993375565MaRDI QIDQ3546313FDOQ3546313
Authors: Andrew M. Pitts 
Publication date: 21 December 2008
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1147954.1147961
Recommendations
- Theorem Proving in Higher Order Logics
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- Publication:4942633
- 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
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65) Inductive definability (03D70)
Cited In (31)
- Rensets and renaming-based recursion for syntax with bindings
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
- Normalization by evaluation and algebraic effects
- Denotational semantics with nominal Scott domains
- Theorem Proving in Higher Order Logics
- 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
- Induction-recursion and initial algebras.
- Mechanized metatheory revisited
- 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
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- A formalized general theory of syntax with bindings: extended version
- Nominal abstraction
- Abstract syntax: substitution and binders
- Foundations of nominal techniques: logic and semantics of variables in abstract syntax
- External and internal syntax of the \(\lambda \)-calculus
- Nominal Lawvere theories: a category theoretic account of equational theories with names
- A simple nominal type theory
- Nominal equational logic
- Formalizing adequacy: a case study for higher-order abstract syntax
- Encoding abstract syntax without fresh names
- A unified treatment of syntax with binders
- Structural recursion with locally scoped names
- Formal SOS-Proofs for the Lambda-Calculus
- Nominal techniques in Isabelle/HOL
- On Normalization by Evaluation for Object Calculi
- Rensets and renaming-based recursion for syntax with bindings extended version
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming
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)
