Olivier Laurent - Game semantics for first-order logic

lmcs:1130 - Logical Methods in Computer Science, October 20, 2010, Volume 6, Issue 4 - https://doi.org/10.2168/LMCS-6(4:3)2010
Game semantics for first-order logicArticle

Authors: Olivier Laurent

    We refine HO/N game semantics with an additional notion of pointer (mu-pointers) and extend it to first-order classical logic with completeness results. We use a Church style extension of Parigot's lambda-mu-calculus to represent proofs of first-order classical logic. We present some relations with Krivine's classical realizability and applications to type isomorphisms.

    https://doi.org/10.2168/LMCS-6(4:3)2010
    Source: arXiv.org:1009.4400
    Volume: Volume 6, Issue 4
    Published on: October 20, 2010
    Imported on: November 7, 2008
    Keywords: Computer Science - Logic in Computer Science,F.3.2, F.4.1, F.3.3
    Licence: arXiv.org - Non-exclusive license to distribute

    4 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 1491 times.
    This article's PDF has been downloaded 446 times.