TY - GEN

T1 - A formal calculus for informal equality with binding

AU - Gabbay, Murdoch

AU - Mathijssen, Aad

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

M3 - Conference contribution

SN - 9783540734437

VL - 4576 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 162

EP - 176

BT - Logic, Language, Information and Computation - 14th International Workshop, WoLLIC 2007, Proceedings

T2 - 14th International Workshop on Logic, Language, Information and Computation

Y2 - 2 July 2007 through 5 July 2007

ER -