@inproceedings{e2534c2867504167ab7cda8fd56cdd29,

title = "A formal calculus for informal equality with binding",

abstract = "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.",

author = "M.J. Gabbay and A.H.J. Mathijssen",

year = "2007",

doi = "10.1007/978-3-540-73445-1_12",

language = "English",

isbn = "978-3-540-73443-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "162--176",

editor = "D. Leivant and {Queiroz, de}, R.J.G.B.",

booktitle = "Proceedings of the 14th Workshop on Logic, Language, Information and Computation (WoLLIC 2007) 2-5 July 2007, Rio de Janeiro, Brasil",

address = "Germany",

note = "conference; WoLLIC 2007, Rio de Janeiro, Brasil; 2007-07-02; 2007-07-05 ; Conference date: 02-07-2007 Through 05-07-2007",

}