Showing cs.PLShow all
2 papers · 1 filter
cs.PL2024
A Coq Mechanization of JavaScript Regular Expression Semantics
Noé De Santo, Aurèle Barrière, Clément Pit-Claudel
We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition…
cs.PL2024
Incremental Proof Development in Dafny with Module-Based Induction
Son Ho, Clément Pit-Claudel
Highly automated theorem provers like Dafny allow users to prove simple properties with little effort, making it easy to quickly sketch proofs. The drawback is that such provers le…