A logic of sequentiality


Churchill, M. and Laird, J., 2010. A logic of sequentiality. In: Dawar, A. and Veith, H., eds. Computer Science Logic (Lecture Notes in Computer Science). Vol. 6247/2. Springer-Verlag, pp. 215-229. (Lecture Notes in Computer Science)

Related documents:

PDF (csl10.pdf) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (456kB) | Preview

    Official URL:


    Game semantics has been used to interpret both proofs and functional programs: an important further development on the programming side has been to model higher-order programs with state by allowing strategies with ``history-sensitive'' behaviour. In this paper, we develop a detailed analysis of the structure of these strategies from a logical perspective by showing that they correspond to proofs in a new kind of affine logic. We describe the semantics of our logic formally by giving a notion of categorical model and an instance based on a simple category of games. Using further categorical properties of this model, we prove a full completeness result: each total strategy is the semantics of a unique cut-free \emph{core} proof in the system. We then use this result to derive an explicit cut-elimination procedure.


    Item Type Book Sections
    CreatorsChurchill, M.and Laird, J.
    EditorsDawar, A.and Veith, H.
    Uncontrolled Keywordsfull completeness, sequentiality, game semantics
    DepartmentsFaculty of Science > Computer Science
    Publisher Statementcsl10.pdf: Proceedings of CSL 2010, Springer Verlag, Editors A. Dawar and H. Veith. The original publication is available at:
    ID Code20970
    Additional InformationProceedings of the 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010


    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...