The Rich World of Game Models

For more info about our services contact : help@bestpfe.com

Table of contents

1 Introduction 
1.1 Semantics of Programming Languages
1.1.1 An (Outdated) Map of Semantics
1.1.2 Semantics Today
1.2 Game Semantics
1.2.1 The Birth of Game Semantics
1.2.2 The Rich World of Game Models
1.3 Motivation and Contributions
1.3.1 Fibred Models
1.3.2 A Bridge Between Models
1.3.3 A Core of Game Models
2 Preliminaries 
2.1 Game Semantics
2.1.1 Hyland-Ong/Nickau Games
2.1.2 Variations on HON Games
2.1.3 Tsukada and Ong’s Model
2.1.4 Abramsky-Jagadeesan-Malacaria Games
2.1.5 Blass Games
2.2 Categorical Preliminaries
2.2.1 Comma and Cocomma Categories
2.2.2 Fibrations
2.2.3 Ends and Coends
2.2.4 Kan Extensions
2.2.5 Presheaf Categories
2.2.6 Exact Squares
2.2.7 Sheaves
2.2.8 Factorisation Systems
2.2.9 Pseudo Double Categories
3 Presheaves and Concurrent Traces 
3.1 Introduction
3.2 From Signatures to Pseudo Double Categories
3.2.1 Signatures and Positions
3.2.2 Execution Steps and Traces
3.2.3 Organising Traces into a Pseudo Double Category
3.2.4 The Category of Execution Traces
3.3 Unfolding
3.4 Perspectives
4 Pseudo Double Categories and Concurrent Game Models 
4.1 Motivation
4.2 Preliminaries
4.3 Signatures for Pseudo Double Categories
4.3.1 A Signature for the -Calculus
4.3.2 Signatures
4.3.3 From Signatures to Pseudo Double Categories
4.3.4 Fibredness and Categories of Plays
4.4 Fibredness
4.4.1 Fibredness through Factorisation Systems
4.4.2 A Little Theory of 1D-Pullbacks and 1D-Injectivity
4.4.3 A Necessary and Sufficient Fibredness Criterion
4.4.4 Cartesian Lifting of Seeds
4.5 Perspectives
5 Justified Sequences in String Diagrams 
5.1 Motivation
5.2 HON Games as String Diagrams
5.2.1 Building the Pseudo Double Category
5.2.2 Categories of Views and Plays
5.2.3 Characterisations of Views and Plays
5.3 The Level of Plays: Intuition
5.3.1 Illustration on an Example
5.3.2 From String Diagrams to Proof Trees
5.3.3 From Proof Trees to Justified Sequences
5.4 The Level of Plays: Formal Proof
5.4.1 Constructing the Functor
5.4.2 Full Faithfulness
5.4.3 Restriction to Views
5.5 The Level of Strategies
5.6 Perspectives
6 Composing Non-Deterministic Strategies 
6.1 Motivation
6.1.1 The Main Ideas
6.1.2 A Technical Point
6.2 Polynomial Functors for Abstract Game Semantics
6.2.1 Plays as a Category-Valued Presheaf
6.2.2 Copycats and Composition as Polynomial Functors
6.2.3 Game Settings, Associativity and Unitality
6.2.4 The Boolean Case
6.3 Applications
6.3.1 Hyland-Ong/Nickau Games
6.3.2 Constraining Strategies
6.3.3 AJM Games: a Partial Answer
6.3.4 A Non-Example: Blass Games
6.4 Innocence
6.4.1 Concurrent Innocence
6.4.2 Prefix-Based Innocence
6.4.3 Boolean Innocence
6.5 Perspectives
A A Proof of View-Analyticity in Tsukada and Ong’s Model