outcome logic in coq

(final project for cs6115)

summary

This repo contains an encoding of Outcome Logic in Coq. We depart from the original paper in two significant ways: we use a big-step operational semantics instead of a denotational semantics and fix our execution model to the powerset monad.

Our main results are in theorems.v, we mechanized the soundness of OL's proof rules, semantic falsification, the equivalence of syntactic and semantic outcome triples, as well as the principle of denial.

We also have an example of our framework in use in malloc.v, where we prove the specificiation of a simple program with malloc that might succeed or have a null dereference error and use the soundness of OL's proof rules to extract the program traces corresponding to both outcomes.

structure

the main files to look at are:

• syntax.v: syntax of command language
• semantics.v: semantics of command language
• assertion.v: outcome assertion language
• ol.v: definition of valid outcome triples
• rules.v: outcome logic proof rules

with most proofs in:

• soundness.v: soundness of individual proof rules
• lemmas.v: general lemmas
• theorems.v: main theorems

there's also:

• state.v: program state
• set.v and vec.v: data structures used for state

dependencies

OCaml version: 5.2.0

Coq version: 8.19.1

building

dune build

or

make -f CoqMakefile