bfcoq

A formally verified Brainfuck compiler in Coq using Hoare logic.

Stages

• Token: Flat lexical tokens
• AST: Inductive loops
• ComIR: Combined sequences of >, <, +, and -
• RelIR: Relative-positioned cell offsets

Installation

bfcoq requires CompCert for its byte type. Using opam, make sure that Coq is installed, then install the CompCert package from the Coq opam repository:

opam install coq
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-compcert