From 53a2b8a2989485e8885d02c786206de84c9fd91d Mon Sep 17 00:00:00 2001
From: Son HO
Date: Tue, 4 Oct 2022 15:56:13 +0200
Subject: Update the README (#3)

* Update the README

* Fix a typo---
 README.md | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index c7b98b5e..279804da 100644
--- a/README.md
+++ b/README.md
@@ -46,8 +46,7 @@ The dependencies can then be installed with the following command:
 opam install ppx_deriving visitors easy_logging zarith yojson core_unix
 ```
 
-When choosing the OCaml compiler version: we compiled Aeneas with version 4.12.1, but any
-recent version should work.
+We use **OCaml 4.12.1**.
 
 Finally, building the project simply requires to run `make` in the top directory.
 
@@ -81,3 +80,10 @@ We have the following limitations, that we plan to address one by one:
   is exploited to implement the synchronisation primitives).
 - **no concurrent execution**: long-term effort. We plan to address coarse-grained
   parallelism as a long-term goal.
+
+## Formalization
+
+The translation has been formalized and published at ICFP2022: [Aeneas: Rust
+verification by functional
+translation](https://dl.acm.org/doi/abs/10.1145/3547647)
+([long version](https://arxiv.org/abs/2206.07185)).
-- 
cgit v1.2.3