A Formal Calculus for Informal Equality with Binding
From MaRDI portal
Publication:3612660
DOI10.1007/978-3-540-73445-1_12zbMath1213.03038MaRDI 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
Two-level Lambda-calculus, Term Equational Systems and Logics, Unity in nominal equational reasoning: the algebra of equality on nominal sets, 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, 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
Uses Software