33 citations · 87 across the 15 of their papers we have counts for
Showing 2023Show all
2 papers · 1 filter
cs.PL2023★ 3 cited
Coqlex: Generating Formally Verified Lexers
Wendlasida Ouedraogo, Gabriel Scherer, Lutz Strassburger
A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of…
cs.LO2023★ 7 cited
Intuitionistic S4 is decidable
Marianna Girlando, Roman Kuznets, Sonia Marin +2
In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years…