# 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
- 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.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