Demo Paper : Coqlex, an approach to generate verified lexers
summary
Coqlex generates lexers in Coq from a list of regular expressions plus actions, proves correctness of the regex engine, match/score computation and lexer consumption semantics, and extracts runnable OCaml code while the code writer itself remains unverified. Actions include position updates, token return, recursive calls and explicit errors, and the system raises a loop detection error for nonterminating specs. It reuses Takashimiyamoto’s regex development, targets extraction to OCaml, and reports being ~10,000× slower than ocamllex but using estimators and simplifications reduces a benchmark gap to ≈5×.
AI-written summary · about