Research

Imperative programs as proofs via game semantics


Reference:

Churchill, M., Laird, J. and McCusker, G., 2011. Imperative programs as proofs via game semantics. In: 26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011. IEEE, pp. 65-74. (Annual Symposium on Logic in Computer Science)

Related documents:

[img]
Preview
PDF (CLM11.pdf) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (384kB) | Preview

    Official URL:

    http://dx.doi.org/10.1109/LICS.2011.19

    Abstract

    Game semantics extends the Curry-Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. We can embed intuitionistic first-order linear logic into this system, as well as an imperative total programming language. The logic makes explicit use of the fact that in the game semantics the exponential can be expressed as a final co algebra. We establish a full completeness theorem for our logic, showing that every bounded strategy is the denotation of a proof.

    Details

    Item Type Book Sections
    CreatorsChurchill, M., Laird, J. and McCusker, G.
    DOI10.1109/LICS.2011.19
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementCLM11.pdf: © 2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
    StatusPublished
    ID Code25204
    Additional Information26th Annual IEEE Symposium on Logic in Computer Science. Toronto, Ontario, Canada. 21–24 June 2011

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...