Commit 6913dac5 authored by Nicola Botta's avatar Nicola Botta
Browse files

Merge branch 'master' of gitlab.pik-potsdam.de:botta/papers

parents b86b77d6 94515098
# On the Correctness of Monadic Backward Induction # On the Correctness of Monadic Backward Induction
This directory contains the Idris development presented in [1]. This directory contains the sources of [1] and some supplementary material.
## Contents ## 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`. - [paper](paper): The literate Idris sources of [1]. The sources 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](code): A condensed version of the source code provided as
code.ipkg`. The folder contains another [README](code/README.md) indicating the content supplementary material to the paper, see [README](code/README.md).
of the individual files.
- [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. - [lwtheory](lwtheory): The lightweight version of the BJI-framework
discussed in [1], together with code for computing optimal
extensions. Requires [2] to type-check, see [README](lwtheory/README.md).
Generated intermediate code and executables can be deleted with `idris The files have been type-checked with Idris 1.3.3-git:ae98085b8 and
--clean code.ipkg` or `idris --clean paper.ipkg`, respectively. IdrisLibs v1.3.3. If you encounter any issues, please get in touch with
Nuria Brede (nubrede@pik-potsdam.de) or Nicola Botta
(botta@pik-potsdam.de).
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). ### Acknowledgment
### Acknowledgement
This is [TiPES](https://www.tipes.dk/) contribution No 37. This is [TiPES](https://www.tipes.dk/) contribution No 37.
This project has received funding from This project has received funding from
...@@ -30,7 +31,7 @@ under grant agreement No 820970. ...@@ -30,7 +31,7 @@ under grant agreement No 820970.
### Timeline ### Timeline
* 2020-06-14: Submitted to the Journal of Functional Programming (JFP) * 2020-07-14: Submitted to the Journal of Functional Programming (JFP)
* 2020-11-02: Decision: Major revision * 2020-11-02: Decision: Major revision
* 2020-02-23: Submitted revised manuscript * 2020-02-23: Submitted revised manuscript
......
package valval package code
modules= Equality modules= Equality
, Sigma , Sigma
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment