Skip to content

Latest commit

 

History

History
22 lines (16 loc) · 612 Bytes

README.md

File metadata and controls

22 lines (16 loc) · 612 Bytes

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