Incorrectness and Adversarial Logic in Rocq

This repository contains an encoding of Incorrectness Logic in Rocq. It will eventually contain an encoding of Adversarial Logic as well.

Milestones

• Encoding IL triples and inference rules
• Soundness of IL This proof was relatively simple once an apt encoding of the denotational semantics presented in the paper was found. There are some slight differences in the DS presented here: primarily the rules for C*, which have been expanded from one computational definition in the paper to two base rules for ok and er executions, and one inductive rule.
• Completeness of IL
• Encoding AL triples and inference rules
• Soundness of AL
• Completeness of AL

Building

# Install Dependencies
opam switch create rocq 4.14.1
opam pin add rocq-runtime 9.1.0
opam install rocq-prover dune

# Clone and build
git clone https://github.com/CharlesAverill/ILAL && cd ILAL
dune build