Finite Automata HF

MaRDI QIDQ40964swMATHFDO

Official website https://www.isa-afp.org/entries/Finite_Automata_HF.html

Cited in

(14)

• Graph theory in Coq: minors, treewidth, and isomorphisms
• Myhill-Nerode
• POSIX Lexing
• Presburger Automata
• Regular Sets
• Hotel Key Card
• Hereditarily Finite Sets
• MSO_Regex_Equivalence
• Regex_Equivalence
• Formally verified algorithms for upper-bounding state space diameters
• Regular language representations in the constructive type theory of Coq
• Hereditarily finite sets in constructive type theory
• Two-Way Automata in Coq
• A formalisation of finite automata using hereditarily finite sets

This page was built for software: Finite Automata HF