Mentions légales du service

Skip to content
Snippets Groups Projects
user avatar
Kenji Maillard authored
a6ecabe8
History
Name Last commit Last update
theories
.gitignore
Makefile
README.md
_CoqProject

The next 700 relational program logics

Prerequisites

The development for this paper is based on the coq development accompanying the paper Dijkstra Monads for All, publicly available at https://gitlab.inria.fr/kmaillar/dijkstra-monads-for-all

This development is contained in the subdirectory theories/Mon and is not a contribution of this artifact.

The prerequisite are inherited from that developement, namely:

  • It requires Coq version 8.10.0

  • The Equation library version 1.2 (on opam under the name coq-equations.1.2(+8.10)) for all the items marked with needs Equations in _CoqProject.

  • For examples based on probabilities, it requires the math-comp-analysis library (version 0.2.2) that can be obtained through opam. Be sure to add the coq-released repo before:

    opam repo add coq-released https://coq.inria.fr/opam/released

The installation step through opam on a fresh switch are thus:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.10.0 coq-equations.1.2+8.10 coq-mathcomp-analysis

Step-by-step Guide

A walkthrough of the paper is provided in theories/RREADME.v explaining how the development maps to the paper.

Run make from this directory to compile all the coq files (this step is needed for the walkthrough). It should succeed displaying only warnings and coq terms.

Organisation of the directories

  • theories/ : root of all the Coq files
  • theories/Mon : external development coming from "Dijkstra monads for all"
  • theories/Relational : development for this paper

Content of the files

In theories/Relational:

  • OrderEnrichedCategory.v: Basic category theory (categories, functors,...) enriched over preorders; Categorical definitions of relative monads and a few constructions on these

  • OrderEnrichedRelativeMonadExamples.v: Concrete instances of categories and relative monads to obtain the simple relational specification monads and the full relational specification monads

  • Rel.v: Main definitions for the relational dependent type theory

  • GenericRulesSimple.v: pure and monadic relational rules in the simpler setting

  • Commutativity.v: Commuting elements of a monad and definition of relational effect observation out of unary effect observation

  • RelationalState.v: specialization to stateful computations with examples of non interference

  • RelationalIO.v: simple relational program logic for IO

  • RelationalNDA.v and RelationalNDD.v : simple relational program logic for non-determinism (angelic and demonic interpretations).

  • RelationalFinProb.v: relational program logic for (independent) finite probabilities

  • RelationalExcSimple.v: specialization to computations raising exceptions

  • GenericRulesComplex.v: pure and monadic relational rules in the full setting

  • RelationalExcFull.v: specialization of the complex setting to exceptions

Axioms and assumptions

Most of the development uses the recent SProp feature of Coq (instead of relying on UIP axiom).

The functional extensionality axiom from Coq's standard library is used extensively in the development, as well as two variations of it with respect to SProp (that can be found in theories/sprop/SPropBase.v, module SPropAxioms). This module also defines the axiom of propositional extensionality for strict propositions.

The use of these axioms can be checked for instance at the end of theories/RREADME.v using Print Assumptions term..

One proof is admitted in Imp.v. Only that file depends on the admitted proof (that was proved on paper).