Alpha-structural recursion and induction

DOI10.1145/1147954.1147961MaRDI QIDQ3546313zbMATH OpenOpenAlexFDO

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)

• Normalization by evaluation and algebraic effects
• Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
• Rensets and renaming-based recursion for syntax with bindings
• 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
• Induction-recursion and initial algebras.
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Binding operators for nominal sets
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Mechanized metatheory revisited
• 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
• Nominal techniques in Isabelle/HOL
• Formal SOS-Proofs for the Lambda-Calculus
• 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)