Alpha equivalence equalities

DOI10.1016/J.TCS.2012.01.030zbMATH Open1244.68030OpenAlexW2063470124MaRDI QIDQ428860FDOQ428860

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

Recommendations

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

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)

Cites Work

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

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

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)