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.

Meta

• Author(s):
  • Peio Borthelle
  • Tom Hirschowitz
  • Guilhem Jaber
  • Yannick Zakowski
• License: GPLv3
• Compatible Coq versions: 8.17
• Additional dependencies:
  • dune
  • Equations
  • Coinduction
  • Alectryon
• Coq namespace: OGS
• Documentation

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