Switch to: References

Citations of:

Polarized games

Annals of Pure and Applied Logic 130 (1-3):79-123 (2004)

Add citations

You must login to add citations.
  1. Totality in arena games.Pierre Clairambault & Russ Harmer - 2010 - Annals of Pure and Applied Logic 161 (5):673-689.
    We tackle the problem of preservation of totality by composition in arena games. We first explain how this problem reduces to a finiteness theorem on what we call pointer structures, similar to the parity pointer functions of Harmer, Hyland and Mélliès and the interaction sequences of Coquand. We discuss how this theorem relates to normalization of linear head reduction in simply-typed lambda-calculus, leading us to a semantic realizability proof à la Kleene of our theorem. We then present another proof of (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Resource modalities in tensor logic.Paul-André Melliès & Nicolas Tabareau - 2010 - Annals of Pure and Applied Logic 161 (5):632-653.
    The description of resources in game semantics has never achieved the simplicity and precision of linear logic, because of the misleading conception that linear logic is more primitive than game semantics. Here, we defend the opposite view, and thus advocate that game semantics is conceptually more primitive than linear logic. This revised point of view leads us to introduce tensor logic, a primitive variant of linear logic where negation is not involutive. After formulating its categorical semantics, we interpret tensor logic (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Imperative programs as proofs via game semantics.Martin Churchill, Jim Laird & Guy McCusker - 2013 - Annals of Pure and Applied Logic 164 (11):1038-1078.
    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. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Lairdʼs sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed first-order (...)
    Download  
     
    Export citation  
     
    Bookmark