Pinned Repositories
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
JumboTrace
optitrust
OptiTrust (w/ RVM case study)
re2-lookbehinds
This fork extends the RE2 regex engine with support for captureless lookbehinds. This implements the algorithm described in the Linear Matching of JavaScript Regular Expressions PLDI 2024 paper (section 4.1).
RegElk
Ocaml Linear Engine for JavaScript Regexes, implementing the algorithms described in Linear Matching of JavaScript Regular Expressions at PLDI24
rvm-compiler-project
SpecMerger
Conformance Checker for Specifications
Warblre
A Coq Mechanization of ECMAScript 2023 Regexes
SYSTEMF's Repositories
epfl-systemf/RegElk
Ocaml Linear Engine for JavaScript Regexes, implementing the algorithms described in Linear Matching of JavaScript Regular Expressions at PLDI24
epfl-systemf/Warblre
A Coq Mechanization of ECMAScript 2023 Regexes
epfl-systemf/re2-lookbehinds
This fork extends the RE2 regex engine with support for captureless lookbehinds. This implements the algorithm described in the Linear Matching of JavaScript Regular Expressions PLDI 2024 paper (section 4.1).
epfl-systemf/JumboTrace
epfl-systemf/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
epfl-systemf/optitrust
OptiTrust (w/ RVM case study)
epfl-systemf/rvm-compiler-project
epfl-systemf/SpecMerger
Conformance Checker for Specifications