Hereditarily Finite Sets

MaRDI QIDQ40963swMATHFDO

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

Described by source

• A formalisation of finite automata using hereditarily finite sets

Cited in

(13)

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

This page was built for software: Hereditarily Finite Sets