Alpha equivalence equalities

DOI10.1016/J.TCS.2012.01.030MaRDI QIDQ428860zbMATH OpenOpenAlexFDO

Authors Roy L. Crole

Publication date 25 June 2012

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2012.01.030

zbMATH Keywords

contextatom\(\alpha \)-equivalence\(\lambda \)-expressionpermutation actionrenamingvariable binding

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• α-Equivalence
• Equality algebras
• Equality algebras
• Tau-equivalence and equipercentile equating
• AF-equivalence relations
• Equivalence theorems
• Pseudo equality algebras

Cites work

• scientific article; zbMATH DE number 1241702 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• (Nominal) unification by recursive descent with triangular substitutions
• A general mathematics of names
• A head-to-head comparison of de Bruijn indices and names
• A new approach to abstract syntax with variable binding
• Binding in nominal equational logic
• Capture-avoiding substitution as a nominal algebra
• Completeness of bisimilarity for contextual equivalence in linear theories
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax
• Nominal Renaming Sets
• Nominal logic, a first order theory of names and binding
• Nominal rewriting
• Nominal unification
• Proof Pearl: De Bruijn Terms Really Do Work
• Some lambda calculus and type theory formalized
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The mechanisation of Barendregt-style equational proofs (the residual perspective)
• The representational adequacy of Hybrid

Cited in

(5)

• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• Algorithms for extended alpha-equivalence and complexity
• Varying alpha
• Equational logic and categorical semantics for multi-languages
• Contextual equivalence for inductive definitions with binders in higher order typed functional programming

Describes a project that uses

Uses Software

• LEGO

This page was built for publication: Alpha equivalence equalities

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q428860)