ZipLex delivers the first verified lexer that is both linear-time and provably invertible between lexing and printing, using token-sequence abstractions, zippers, and a verified hash table in Stainless.
Title resolution pending
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
fields
cs.PL 2years
2025 2verdicts
ACCEPT 2representative citing papers
A Rocq-mechanized semantics for JavaScript regex with backtracking, proven equivalent to an ECMAScript embedding, then used to verify contextual equivalence of rewrites and to prove correctness of the PikeVM algorithm.
citing papers explorer
-
Formally Verified Linear-Time Invertible Lexing
ZipLex delivers the first verified lexer that is both linear-time and provably invertible between lexing and printing, using token-sequence abstractions, zippers, and a verified hash table in Stainless.
-
Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
A Rocq-mechanized semantics for JavaScript regex with backtracking, proven equivalent to an ECMAScript embedding, then used to verify contextual equivalence of rewrites and to prove correctness of the PikeVM algorithm.