Update README.

2021.On the Correctness of Monadic Backward Induction/README.md

+# On the Correctness of Monadic Backward Induction
+
+This directory contains the Idris development presented in [1].
+
+## Contents
+
+- [paper](./paper): The paper is written in literate Idris and its sources can be found in this folder. They can be compiled to pdf using `make` and type-checked using the command `idris --checkpkg paper.ipkg`.
+
+- [code](./code): This folder contains a condensed version of the relevant source code (also provided as supplementary material to the paper). It can be type-checked using the command `idris --checkpkg
+code.ipkg`. The folder contains another [README](./code/README.md) indicating the content
+of the individual files.
+
+- [examples](./examples): This folder contains the lightweight version of the BJI-framework discussed in [1], augmented with the necessary implementations for computing optimal extensions and using the framework's backward induction algorithm. It needs the library from [2] to type-check. The folder contains another [README](./examples/README.md) with instructions.
+
+Generated intermediate code and executables can be deleted with `idris
+--clean code.ipkg` or `idris --clean paper.ipkg`, respectively.
+
+The literate Idris files have been successfully type-checked with Idris 1.3.2.
+
+If you encounter any issues, please get in touch with [Nicola Botta](botta@pik-potsdam.de) or [Nuria Brede](nubrede@pik-potsdam.de).
+
+
+### Acknowledgement
+
+This is [TiPES](https://www.tipes.dk/) contribution No 37.
+This project has received funding from
+the European Union’s Horizon 2020 research and innovation programme
+under grant agreement No 820970.
+
+
+### Timeline
+
+* 2020-06-14: Submitted to the Journal of Functional Programming (JFP)
+* 2020-11-02: Decision: Major revision
+* 2020-02-23: TODO: Submit revised manuscript
+
+---
+
+[1] Nuria Brede and Nicola Botta. (2021)
+    On the Correctness of Monadic Backward Induction.
+
+[2] Nicola Botta. (2016-21)
+    [IdrisLibs](https://gitlab.pik-potsdam.de/botta/IdrisLibs)
+
+
+[3] Botta, N., Jansson, P., Ionescu, C. (2017).
+    Contributions to a    computational theory of policy advice and avoidability. J. Funct. Program. 27:e23.

2021.On the Correctness of Monadic Backwards Induction/README.md

-* To type check About.lidr (or other literate Idris file) with idris
-  (version 1.3.3) in your path:
-
-    + Download IdrisLibs or IdrisLibs2 from [1] or [2].
-
-    + enter "idris -i $IDRISLIBS --sourcepath $IDRISLIBS --allow-capitalized-pattern-variables About.lidr
-
-  where IDRISLIBS is the path of IdrisLibs or IdrisLibs2.
-
-* To generate a PostScript version of the paper:
-
-    + enter "make" in the command line.
-
-* If you encounter any issue, please get in touch (botta@pik-potsdam.de).
-
-
-* [1] https://gitlab.pik-potsdam.de/botta/IdrisLibs
-
-* [2] https://gitlab.pik-potsdam.de/botta/IdrisLibs2