A Formal Calculus for Informal Equality with Binding

DOI10.1007/978-3-540-73445-1_12MaRDI QIDQ3612660zbMATH OpenOpenAlexFDO

Authors Aad Mathijssen, Murdoch J. Gabbay

Publication date 10 March 2009

Published in Logic, Language, Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73445-1_12

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Logic in computer science (03B70)

Recommendations

• Nominal (universal) algebra: equational logic with names and binding
• External and internal syntax of the \(\lambda \)-calculus
• A Nominal Axiomatization of the Lambda Calculus
• Binding in nominal equational logic
• Two-level lambda-calculus

Cited in

(11)

• On the construction of free algebras for equational systems
• The lambda-context calculus (extended version)
• Two cotensors in one: presentations of algebraic theories for local state and fresh names
• Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
• Unity in nominal equational reasoning: the algebra of equality on nominal sets
• Two-level lambda-calculus
• Term equational systems and logics (extended abstract)
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness
• Capture-avoiding substitution as a nominal algebra
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

Describes a project that uses

Uses Software

• mCRL2
• Twelf

This page was built for publication: A Formal Calculus for Informal Equality with Binding

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