Program Proof

For studying program proving with OCaml implementations.

Contents

• A small language
• Typing as proving

Command

Build

dune build

Test

dune runtest

Execution

dune exec program_proof

References

• Samuel Mimram. PROGRAM = PROOF
• Benjamin C. Pierce. Types and Programming Languages
• Rob Nederpelt, Herman Geuvers. Type Theory and Formal Proof: An Introduction
• dune