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.
In CPP ’22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
fields
cs.PL 3representative 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.
Generalizes rely-guarantee to parametric memory models and presents Piccolo, the first such logic for causally consistent shared memory using potential-based operational semantics.
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.
-
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
Generalizes rely-guarantee to parametric memory models and presents Piccolo, the first such logic for causally consistent shared memory using potential-based operational semantics.