Alpha-structural recursion and induction

DOI10.1145/1147954.1147961zbMath1326.68180OpenAlexW1993375565MaRDI QIDQ3546313

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) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Inductive definability (03D70)

Related Items (29)

Normalization by evaluation and algebraic effects ⋮ Formal metatheory of the lambda calculus using Stoughton's substitution ⋮ A unified treatment of syntax with binders ⋮ Encoding abstract syntax without fresh names ⋮ Formalizing adequacy: a case study for higher-order abstract syntax ⋮ Nominal abstraction ⋮ On Normalization by Evaluation for Object Calculi ⋮ A formalized general theory of syntax with bindings ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Nominal techniques in Isabelle/HOL ⋮ Nominal Lawvere theories: a category theoretic account of equational theories with names ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Binding operators for nominal sets ⋮ Alpha-structural induction and recursion for the lambda calculus in constructive type theory ⋮ Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax ⋮ Structural recursion with locally scoped names ⋮ Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus ⋮ External and internal syntax of the \(\lambda \)-calculus ⋮ Formal SOS-Proofs for the Lambda-Calculus ⋮ A Simple Nominal Type Theory ⋮ Mechanized metatheory revisited ⋮ Denotational Semantics with Nominal Scott Domains ⋮ Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory ⋮ Nominal Equational Logic ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Abstract Syntax: Substitution and Binders ⋮ 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