A formal calculus for informal equality with binding

M.J. Gabbay, A.H.J. Mathijssen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    23 Citations (Scopus)
    81 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationProceedings of the 14th Workshop on Logic, Language, Information and Computation (WoLLIC 2007) 2-5 July 2007, Rio de Janeiro, Brasil
    EditorsD. Leivant, R.J.G.B. Queiroz, de
    Place of PublicationBerlin, Germany
    PublisherSpringer
    Pages162-176
    ISBN (Print)978-3-540-73443-7
    DOIs
    Publication statusPublished - 2007
    Eventconference; WoLLIC 2007, Rio de Janeiro, Brasil; 2007-07-02; 2007-07-05 -
    Duration: 2 Jul 20075 Jul 2007

    Publication series

    NameLecture Notes in Computer Science
    Volume4576
    ISSN (Print)0302-9743

    Conference

    Conferenceconference; WoLLIC 2007, Rio de Janeiro, Brasil; 2007-07-02; 2007-07-05
    Period2/07/075/07/07
    OtherWoLLIC 2007, Rio de Janeiro, Brasil

    Fingerprint

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

    Cite this