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

zbMATH Keywords

recursioninductionbindersnamesabstract syntax

Mathematics Subject Classification ID

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)

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

Cited in

(31)

• External and internal syntax of the \(\lambda \)-calculus
• A formalized general theory of syntax with bindings: extended version
• Structural recursion with locally scoped names
• Nominal equational logic
• Abstract syntax: substitution and binders
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Formal SOS-Proofs for the Lambda-Calculus
• Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
• Denotational semantics with nominal Scott domains
• Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
• Formalizing adequacy: a case study for higher-order abstract syntax
• Nominal techniques in Isabelle/HOL
• Nominal Lawvere theories: a category theoretic account of equational theories with names
• Nominal abstraction
• On Normalization by Evaluation for Object Calculi
• Encoding abstract syntax without fresh names
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Induction-recursion and initial algebras.
• Rensets and renaming-based recursion for syntax with bindings extended version
• A unified treatment of syntax with binders
• Mechanized metatheory revisited
• Binding operators for nominal sets
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Rensets and renaming-based recursion for syntax with bindings
• Contextual equivalence for inductive definitions with binders in higher order typed functional programming
• Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
• Theorem Proving in Higher Order Logics
• Normalization by evaluation and algebraic effects
• A simple nominal type theory
• A formalized general theory of syntax with bindings
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax

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)