2.6. Regular Expression Compiler (Paper Section 4.3)

The most sophisticated example compiles regular expressions to x86 machine code by composing with Braibant and Pous's Kleene algebra formalization:

Regular expression → DFA (from ATBR library)
DFA → x86 jump table (new compiler)

The compiler has a certified correctness theorem:

Lemma DFA_to_x86_correct (w: seq DWORD) :
  (* If it's safe to jump to acc when DFA accepts... *)
  (* and safe to jump to rej when DFA rejects... *)
  (* then it's safe to run the compiled code *)

This demonstrates horizontal composition of verified DSL compilers—a key benefit of working within a proof assistant.