Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
examples
monad_base
Holmakefile
README.md
cfMonadLib.sml
cfMonadScript.sml
ml_monadStoreLib.sig
ml_monadStoreLib.sml
ml_monadStoreScript.sml
ml_monad_translatorBaseScript.sml
ml_monad_translatorLib.sig
ml_monad_translatorLib.sml
ml_monad_translatorScript.sml
readmePrefix

README.md

Extensions to the proof-producing translator to support stateful/imperative (monadic) HOL functions.

cfMonadLib.sml: Automation that converts between judgements used by CF and judgements used by the monadic translator.

cfMonadScript.sml: Proves a connection between the monadic translator's ArrowP judgement and CF's app judgement.

examples: This directory contains example applications of the monadic translator. These examples serve as test cases of the monadic translator.

ml_monadStoreLib.sml: Automation that derives lemmas about arrays and references for use by the monadic translator.

ml_monadStoreScript.sml: This file defines theorems and lemma used in the ml_monadStoreLib

ml_monad_translatorBaseScript.sml: Assertions about references and arrays are defined. Lemmas for these are proved, including reasoning in separation logic.

ml_monad_translatorLib.sml: The ML code that implements the main part of the monadic translator.

ml_monad_translatorScript.sml: Defines EvalM and other judgements that are central to the monadic translator.

monad_base: The state-and-exception monad that is used by the proof-producing translator for monadic HOL functions.