A formal calculus for informal equality with binding

Murdoch Gabbay, Aad Mathijssen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

37 Citations (Scopus)


In informal mathematical usage we often reason using languages with binding. We usually find ourselves placing capture-avoidance constraints on where variables can and cannot occur free. We describe a logical derivation system which allows a direct formalisation of such assertions, along with a direct formalisation of their constraints. We base our logic on equality, probably the simplest available judgement form. In spite of this, we can axiomatise systems of logic and computation such as first-order logic or the lambda-calculus in a very direct and natural way. We investigate the theory of derivations, prove a suitable semantics sound and complete, and discuss existing and future research. © Springer-Verlag Berlin Heidelberg 2007.

Original languageEnglish
Title of host publicationLogic, Language, Information and Computation - 14th International Workshop, WoLLIC 2007, Proceedings
Number of pages15
Volume4576 LNCS
Publication statusPublished - 2007
Event14th International Workshop on Logic, Language, Information and Computation - Rio de Janeiro, Brazil
Duration: 2 Jul 20075 Jul 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4576 LNCS
ISSN (Print)0302-9743


Conference14th International Workshop on Logic, Language, Information and Computation
Abbreviated titleWoLLIC
CityRio de Janeiro


Dive into the research topics of 'A formal calculus for informal equality with binding'. Together they form a unique fingerprint.

Cite this