Regular Language Representations in the Constructive Type Theory of Coq
In: ISSN: 0168-7433, 2018
Online
academicJournal
Zugriff:
International audience ; We explore the theory of regular language representations in the constructive type theory of Coq. We cover various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. We give translations between all representations, show decidability results, and provide operations for various closure properties. Our results include a constructive decidability proof for the logic WS1S, a constructive refinement of the Myhill-Nerode characterization of regularity, and translations from two-way automata to one-way automata with verified upper bounds for the increase in size. All results are verified with an accompanying Coq development of about 3000 lines.
| Titel: |
Regular Language Representations in the Constructive Type Theory of Coq
|
|---|---|
| Autor/in / Beteiligte Person: | Doczkal, Christian ; Smolka, Gert ; Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS) ; Saarland University Saarbrücken ; ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010) ; European Project: 678157,H2020,ERC-2015-STG,CoVeCe(2016) |
| Link: | |
| Zeitschrift: | ISSN: 0168-7433, 2018 |
| Veröffentlichung: | HAL CCSD ; Springer Verlag, 2018 |
| Medientyp: | academicJournal |
| DOI: | 10.1007/s10817-018-9460-x |
| Schlagwort: |
|
| Sonstiges: |
|