module Index where -- Agda formalisation of the logic WS -- as introduced in "A Logic of Sequentiality", CSL 2010 -- by Martin Churchill and Jim Laird -- Agda formalisation by Martin Churchill and Makoto Takeyama. -- Section 1 : Foundations -- Formalisation of game semantics in Agda open import Game -- Formalisation of the logic WS open import WS-Syn -- Formalisation of the game semantics of WS open import WS-Sem -- Reification of strategies as core proofs (and thus normalisation of -- proofs to core proofs, via the semantics) open import WS-Comp -- Cut elimination procedure for core proofs open import WS-Cut -- Examples of WS proofs, including bounded exponentials, coroutines, -- ground store... open import WS-Exp open import WS-SCIL-Consts -- A Finitary Language and its game semantics, via WS open import FinLang -- Section 2 : Interaction -- Converts a formula into an *annotated* game, where moves are -- annotated with the corresponding subformulas open import WS-Annot -- Parsing and Printing Games and Formulas open import IOWS open import IOGame -- A module to "run" a strategy, where the computer plays the role of -- Player and the user is invited to play the role of Opponent open import RunStrategy -- A module where the user types in a formula F and the program prints -- the corresponding annotated game open import ParsePrintLoop -- A module to turn proofs in WS into Latex open import WS-Tex -- Some Examples open import Interaction -- Infinite versions! open import Game-CoreInf