a-Logic With Arrows

DOI10.1016/j.entcs.2008.06.031zbMath1283.03064OpenAlexW2110141919MaRDI QIDQ5403474

Michael Gabbay, Murdoch James Gabbay

Publication date: 26 March 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.06.031

zbMATH Keywords

completenessfirst-order logicsoundnesslambda-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Logic programming (68N17) Combinatory logic and lambda calculus (03B40)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Capture-avoiding substitution as a nominal algebra
• Natural deduction and arbitrary objects
• Confluence by decreasing diagrams
• On the algebraic models of lambda calculus
• Rewriting logic: Roadmap and bibliography
• Handbook of philosophical logic. Vol. 18
• Nominal logic, a first order theory of names and binding
• Nominal rewriting
• Generalized definitional reflection and the inversion principle
• On a monadic semantics for freshness
• Some improvements to Turner's algorithm for bracket abstraction
• Capture-Avoiding Substitution as a Nominal Algebra
• Term Rewriting and All That
• On the Notion of Substitution
• Topological incompleteness and order incompleteness of the lambda calculus
• A proof theory for generic judgments
• Theorem Proving in Higher Order Logics