README.md 1.82 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4
# Prerequisites

This version is known to compile with:

Dan Frumin's avatar
Dan Frumin committed
5
 - Coq 8.6.1
Robbert Krebbers's avatar
Robbert Krebbers committed
6
 - Ssreflect 1.6
7
 - Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
Robbert Krebbers's avatar
Robbert Krebbers committed
8
 - std++ version [24aef2fea9481e65d1f6658005ddde25ae9a64ee](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/24aef2fea9481e65d1f6658005ddde25ae9a64ee)
Dan Frumin's avatar
Dan Frumin committed
9
 - Iris version [4be0320e9ff9122e90fa5af60e6a02e81eaffa33](https://gitlab.mpi-sws.org/FP/iris-coq/tree/4be0320e9ff9122e90fa5af60e6a02e81eaffa33)
10 11 12

# Compilation

Dan Frumin's avatar
Dan Frumin committed
13
Make sure that all the dependencies are installed and run `make`.
14 15 16 17 18 19

# Documentation

See [refman.md](docs/refman.md).

Work in progress.
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37

# Structure

- `logrel.v` - exports all the modules required to perform refinement proofs such as those in the `example/` folder
- `F_mu_ref_conc` - definition of the object language
- `examples` - example refinements
- `logrel` contains modules related to the relational interpretation
  + `threadpool.v` - definitions for the ghost threadpool RA
  + `rules_threadpool.v` - symbolic execution in the threadpool
  + `proofmode/tactics_threadpool.v` - tactics for preforming symbolic execution in the threadpool
  + `semtypes.v` - interpretation of types/semantics in terms of values
  + `logrel_binary.v` - interpretation of sequents/semantics in terms of open expressions
  + `rules.v` - symbolic execution rules for the relational interpretation
  + `proofmode/tactics_rel.v` - tactics for performing symbolic execution in the relational interpretation
  + `fundamental_binary.v` - compatibility lemmas and the fundamental theorem of logical relations
  + `contextual_refinement.v` - proof that logical relations are closed under contextual refinement
  + `soundness_binary.v` - typesafety and contextual refinement proofs for terms in the relational interpretation  
- `prelude` - some files shares by the whole development