THIS PROJECT HAS MOVED TO

https://gitlab.mpi-sws.org/iris/reloc

The code here remains for historical reasons . . . .

Prerequisites

This version is known to compile with:

• Coq 8.7.2
• Ssreflect 1.6.4
• Autosubst branch coq86-devel
• std++ version 32570aa6e0d04633047d9fddb3cf8da1748d9695
• Iris version 7e33a806f2cd8da0409f1e5a13126317afd23e3d

Compilation

Make sure that all the dependencies are installed and run make.

Documentation

See refman.md.

Work in progress.

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
  • 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
  • symbol.v and generative.v - generative ADTs examples from the "State-Dependent Representational Independence" 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
  • 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 - type safety and contextual refinement proofs for terms in the relational interpretation
• prelude - some files shares by the whole development