README.md 2.06 KB
Newer Older
Nuria Brede's avatar
Nuria Brede committed
1
2
3
4
5
6
# On the Correctness of Monadic Backward Induction

This directory contains the Idris development presented in [1].

## Contents

Nuria Brede's avatar
Nuria Brede committed
7
- [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`.
Nuria Brede's avatar
Nuria Brede committed
8

Nuria Brede's avatar
Nuria Brede committed
9
10
- [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
Nuria Brede's avatar
Nuria Brede committed
11
12
of the individual files.

Nuria Brede's avatar
Nuria Brede committed
13
- [lwtheory](lwtheory): 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](lwtheory/README.md) with instructions.
Nuria Brede's avatar
Nuria Brede committed
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32

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

Nuria Brede's avatar
Nuria Brede committed
33
* 2020-07-14: Submitted to the Journal of Functional Programming (JFP)
Nuria Brede's avatar
Nuria Brede committed
34
* 2020-11-02: Decision: Major revision
Nuria Brede's avatar
Update.    
Nuria Brede committed
35
* 2020-02-23: Submitted revised manuscript
Nuria Brede's avatar
Nuria Brede committed
36
37
38
39
40
41
42
43
44
45
46
47

---

[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.