Permalink
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
37 lines (27 sloc) 1.36 KB

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.