README.md and opam file

README.md

 # Aneris
 
-Aneris is a program logic build on the Iris program logic framework for
-developing and verifying distributed systems.
+Aneris is a programming language and a higher-order distributed concurrent
+separation logic for developing and verifying distributed systems with
+facilities for modular specification and verification of partial correctness
+properties. The logic is built using the [Iris](https://iris-project.org)
+program logic framework and mechanized in the Coq proof assistant.
 
 ## Compiling
 
-The development is known to compile with
-
-- `coq`: see the `opam` file
-- `coq-iris` : see the `opam` file
-- `coq-stdpp` : see the `opam` file
-- `coq-iris-string-ident`
-
 To install the dependencies, you have to add the following opam repositories:
 
     opam repo add coq-released https://coq.inria.fr/opam/released
     opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 
 Once you got opam set up, run `opam update` followed by `make build-dep` to
-install the right versions of the dependencies.
+install the right versions of the dependencies as specified in the `aneris.opam`
+file.
 
-Next, clone external submodule dependencies using
+Next, clone the external submodule dependencies using
 
     git submodule update --init --recursive
 
@@ -29,9 +26,9 @@ Alternatively, clone the repository using the `--recurse-submodules` flag.
 Run `make -jN` to build the full development, where `N` is the number of your
 CPU cores.
 
-## Updating dependencies
+## Updating git submodule dependencies
 
-To pull the latest submodules dependencies as committed to the repository, run
+To pull the latest git submodule dependencies as committed to the repository, run
 
     git submodule update --recursive
 
@@ -42,10 +39,12 @@ changes. However, it does not apply the changes. To update the dependencies run
 
 Remember to commit submodule updates to the repository.
 
-## Directory structure
-
-TODO
-
-## Case studies
+## Publications
 
-See [aneris-examples](https://bitbucket.org/logsem/aneris-examples).
+Aneris was initially presented in the ESOP 2020 paper [Aneris: A Mechanised
+Logic for Modular Reasoning about Distributed
+Systems](https://link.springer.com/chapter/10.1007/978-3-030-44914-8_13) by
+Morten Krogh-Jespersen, [Amin Timany](https://tildeweb.au.dk/au571806/), Marit
+Edna Ohlenbusch, [Simon Oddershede Gregersen](https://cs.au.dk/~gregersen/), and
+[Lars Birkedal](https://cs.au.dk/~birke/). Since then, the duplicate protection
+assumption as described in the paper has been relaxed.

opam → aneris.opam

 opam-version: "2.0"
-name: "coq-aneris"
-synopsis: "This is the Coq development of the Aneris program logic"
+synopsis: "Coq development of the Aneris program logic"
 maintainer: "Simon Gregersen <gregersen@cs.au.dk>"
 authors: "The Aneris Team"
-homepage: "https://iris-project.org/"
-dev-repo: "git+https://bitbucket.org/logsem/aneris.git"
-bug-reports: "https://bitbucket.org/logsem/aneris/issues"
+license: "MIT"
+homepage: "https://github.com/logsem/aneris"
+dev-repo: "git+https://github.com/logsem/aneris.git"
+bug-reports: "https://github.com/logsem/aneris/issues"
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" { (= "8.12.0") | (= "dev") }
-  "coq-iris" { (= "dev.2020-08-07.2.b2b558ac") | (= "dev") }
-  "coq-stdpp" { (= "dev.2020-08-07.0.67db2f24") | (= "dev") }
-  "coq-iris-string-ident" { (= "dev") | (= "dev") }
+  "coq-iris" { (= "dev.2020-09-03.2.26739725") | (= "dev") }
+  "coq-stdpp" { (= "dev.2020-09-02.0.897b954e") | (= "dev") }
+  "coq-iris-string-ident" { (= "dev")  }
 ]