README

README.md

 # LAMBDA-RUST COQ DEVELOPMENT
 
-This is the Coq formalization of lambda-Rust.
+This is the Coq development accompanying lambda-Rust.
 
 ## Prerequisites
 
@@ -11,21 +11,40 @@ This version is known to compile with:
  - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
 
 The easiest way to install the correct versions of the dependencies is through
-opam.  Once you got opam set up, just run `make build-dep` to install the right
-versions of the dependencies.  When the dependencies change (e.g., a newer
-version of Iris is needed), just run `make build-dep` again.
+opam.  Coq packages are available on the coq-released repository, set up by the
+command:
 
-Alternatively, you can manually determine the required Iris commit by consulting
-the `opam.pins` file.
+    opam repo add coq-released https://coq.inria.fr/opam/released
+
+Once you got opam set up, just run `make build-dep` to install the right
+versions of the dependencies.  When the dependencies change, just run `make
+build-dep` again.
 
 ## Building Instructions
 
 Run `make` to build the full development.
 
+## Structure
+
+* The folder [lang](theories/lang) contains the formalization of the lambda-Rust
+  core language, including the theorem showing that programs with data races get
+  stuck.
+* The folder [lifetime](theories/lifetime) proves the rules of the lifetime
+  logic, including derived constructions like (non-)atomic persistent borrows.
+* The folder [typing](theories/typing) defines the domain of semantic types,
+  interpretations of all the judgments, as well as proofs of all typing rules.
+  * The subfolder [examples](theories/typing/examples) shows how the examples
+    from the technical appendix can be type-checked in Coq.
+  * The subfolder [lib](theories/typing/lib) contains proofs of safety of some
+    unsafely implement types from the Rust standard library and some user
+    crates: `Cell`, `RefCell`, `Rc`, `Arc`, `Mutex`, `RwLock`, `mem::swap`,
+    `thread::spawn`, `take_mut::take`, `alias::once` as well as converting `&&T`
+    to `&Box<T>`.
+
 ## For Developers: How to update the Iris dependency
 
-- Do the change in Iris, push it.
-- In lambdaRust, change opam.pins to point to the new commit.
-- Run "make build-dep" (in lambdaRust) to install the new version of Iris.
-- You may have to do "make clean" as Coq will likely complain about .vo file
+* Do the change in Iris, push it.
+* In lambdaRust, change opam.pins to point to the new commit.
+* Run "make build-dep" (in lambdaRust) to install the new version of Iris.
+* You may have to do "make clean" as Coq will likely complain about .vo file
   mismatches.