Commit 39800179 authored by Dan Frumin's avatar Dan Frumin

Add more information about the project structure

parent f2f3b6bf
......@@ -22,7 +22,24 @@ Work in progress.
- `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
+ `binder.v` - auxiliary lemmas/instances for binders
+ `lang.v` - definition of the object language with operational semantics
+ `subst.v` - parallel substitution
+ `notation.v` - useful Coq notation for the language
+ `typing.v` - the type system
+ `reflection.v` - a refined version of the target language for proving certain properties by computation
+ `rules.v` - WP calculus
+ `adequacy.v` - soundness of the WP rules
+ `context_refinement.v` - definition of contextual refinement
+ `pureexec.v`, `tactics.v` - instances and tactics for doing symbolic execution
- `examples` - example refinements
+ `bit.v` - "representation independence example" for a simple bit interface
+ `par.v` - compatibility lemma for parallel composition
+ `or.v` - expressing non-determinism with concurrency
+ `counter.v` - fine-grained concurrent counter refines coarse-grained concurrent counter
+ `stack/module_refinement.v`, `stack/refinement.v` - Treiber stack refines sequential stack
+ `stack/helping.v` - stack with helping refines sequential stack
+ `various.v` - some examples with higher-order functions with local state, in the style of "The effects of higher-order state and control on local relational reasoning" paper
- `logrel` contains modules related to the relational interpretation
+ `threadpool.v` - definitions for the ghost threadpool RA
+ `rules_threadpool.v` - symbolic execution in the threadpool
......@@ -33,5 +50,5 @@ Work in progress.
+ `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
+ `soundness_binary.v` - type safety and contextual refinement proofs for terms in the relational interpretation
- `prelude` - some files shares by the whole development
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment