A Constructive Theory of Regular Languages in Coq
From MaRDI portal
Publication:2938041
DOI10.1007/978-3-319-03545-1_6zbMath1426.68143OpenAlexW95934751MaRDI QIDQ2938041
Gert Smolka, Christian Doczkal, Jan-Oliver Kaiser
Publication date: 13 January 2015
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-03545-1_6
Formal languages and automata (68Q45) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
A Formalisation of Finite Automata Using Hereditarily Finite Sets, Formally verified algorithms for upper-bounding state space diameters, Regular language representations in the constructive type theory of Coq, A Verified Compositional Algorithm for AI Planning, On the Formalization of Some Results of Context-Free Language Theory, Two-Way Automata in Coq, A formalisation of the Myhill-Nerode theorem based on regular expressions
Uses Software