A Constructive Theory of Regular Languages in Coq
No abstract available.
DOI 10.1007/978-3-319-03545-1_6
Related papers
- Completeness and decidability of converse PDL in the constructive type theory of Coq CPP 2018
- Verified and Efficient Matching of Regular Expressions with Lookaround CPP 2025
- Symbolic Automata: Omega-Regularity Modulo Theories POPL 2025
- Large model constructions for second-order ZF in dependent type theory CPP 2018
- Symbolic Boolean derivatives for efficiently solving extended regular expression constraints PLDI 2021
- On synthetic undecidability in coq, with an application to the entscheidungsproblem CPP 2019
- Is sized typing for Coq practical? JFP 2023
- Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting TACAS 2020