An abstract, certified account of operational game semantics

This is the companion artifact to the paper. The main contributions of this library are:

an independent implementation of an indexed counterpart to the itree
library with support for guarded and eventually guarded recursion
an abstract OGS model of an axiomatised language proven sound w.r.t.
substitution equivalence
several instantiations of this abstract result to concrete
languages: simply-typed lambda-calculus with recursive functions,
untyped lambda calculus, Downen and Ariola's polarized system D and
system L.

Building instructions

Installing dependencies

Download the project with

git clone https://github.com/lapin0t/ogs.git
cd ogs

We stress that the development has been only checked to compile against these specific dependencies. In particular, it does not compiled at the moment against latest version of coq-coinduction due to major changes in the interface.

Installing the opam dependencies automatically:

opam install --deps-only .

or manually:

opam pin coq 8.17
opam pin coq-equations 1.3
opam pin coq-coinduction 1.6

Building the project

dune build

Alectryon documentation

To build the html documentation, first install Alectryon:

opam install "coq-serapi==8.17.0+0.17.1"
python3 -m pip install --user alectryon

Then build with:

make doc

You can start a local web server to view it with:

make serve

Content

Structure of the repository

The Coq development is contained in the theory directory, which has the following structure, in approximate order of dependency.

Readme.v: this file
Prelude.v: imports and setup
Utils directory: general utilities
- Rel.v: generalities for relations over indexed types
- Psh.v: generalities for type families
Ctx directory: general theory of contexts and variables
- Family.v: definition of scoped and sorted
  families
- Abstract.v: definition of context and variable
  structure
- Assignment.v: generic definition of
  assignments
- Renaming.v: generic definition of renamings
- Ctx.v: definition of concrete contexts and DeBruijn
  indices
- Covering.v: concrete context structure for
  Ctx.v
- DirectSum.v: direct sum of context structures
- Subset.v: sub context structure
ITree directory: implementation of a variant of interaction trees
over indexed types
- Event.v: indexed events parameterizing the
  interactions of an itree
- ITree.v: coinductive definition
- Eq.v: strong and weak bisimilarity over interaction
  trees
- Structure.v: combinators (definitions)
- Properties.v: general theory
- Guarded.v: (eventually) guarded equations and
  iterations over them
- Delay.v: definition of the delay monad (as a
  special case of trees)
OGS directory: construction of a sound OGS model for an abstract
language
- Subst.v: axiomatization of substitution monoid,
  substitution module
- Obs.v: axiomatization of observation structure,
  normal forms
- Machine.v: axiomatization of evaluation
  structures, language machine
- Game.v: abstract game and OGS game definition
- Strategy.v: machine strategy and composition
- CompGuarded.v: proof of eventual guardedness
  of the composition of strategies
- Adequacy.v: proof of adequacy of composition
- Congruence.v: proof of congruence of
  composition
- Soundness.v: proof of soundness of the OGS
Examples directory: concrete instances of the generic construction
- STLC_CBV.v: simply typed, call by value, lambda
  calculus
- ULC_CBV.v: untyped, call by value, lambda
  calculus
- SystemL_CBV.v: mu-mu-tilde calculus variant
  System L, in call by value
- SystemD.v: mu-mu-tilde calculus variant System
  D, polarized

Axioms

The whole development relies only on axiom K, a conventional and sound axiom from Coq's standard library (more precisely, Eq_rect_eq.rect_eq.

This can be double checked as follows:

for the abstract result of soundness of the OGS by running
Print Assumptions ogs_correction. at the end of OGS/Soundness.v
for any particular example, for instance by running
Print Assumptions stlc_ciu_correct. at the end of
Example/CBVTyped.v