A Formal Calculus for Informal Equality with Binding
From MaRDI portal
Publication:3612660
DOI10.1007/978-3-540-73445-1_12zbMath1213.03038OpenAlexW2134022633MaRDI QIDQ3612660
Aad Mathijssen, Murdoch James 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
Related Items (11)
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 ⋮ Capture-avoiding substitution as a nominal algebra ⋮ Term Equational Systems and Logics ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ 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 ⋮ Two Cotensors in One: Presentations of Algebraic Theories for Local State and Fresh Names ⋮ On the construction of free algebras for equational systems ⋮ Two-level Lambda-calculus ⋮ The lambda-context calculus (extended version)
Uses Software
This page was built for publication: A Formal Calculus for Informal Equality with Binding
