A constructive theory of regular languages in Coq

DOI10.1007/978-3-319-03545-1_6MaRDI QIDQ2938041zbMATH OpenOpenAlexFDO

Authors Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka

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

zbMATH Keywords

Coqfinite automataMyhill-Neroderegular expressionsregular languagesSsreflect

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Regular language representations in the constructive type theory of Coq
• Partial derivative automata formalized in Coq
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Deciding regular expressions (in-)equivalence in Coq
• A formalisation of the Myhill-Nerode theorem based on regular expressions

Cited in

(16)

• Formally verified algorithms for upper-bounding state space diameters
• Regular language representations in the constructive type theory of Coq
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• scientific article; zbMATH DE number 1670817 (Why is no real title available?)
• On the formalization of some results of context-free language theory
• Two-Way Automata in Coq
• Certified parsing of regular languages
• A mechanized theory of regular trees in dependent type theory
• Partial derivative automata formalized in Coq
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• A formalisation of finite automata using hereditarily finite sets
• Simulating finite Eilenberg machines with a reactive engine
• A Verified Compositional Algorithm for AI Planning
• Pumping, with or without choice
• Brzozowski's algorithm for automata minimization verified in Coq
• A fixed point characterization of cofinite languages

Describes a project that uses

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: A constructive theory of regular languages in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938041)