Hereditarily Finite Sets

MaRDI QIDQ40963swMATHFDO

Authors Lawrence C. Paulson

Publication date 17 November 2013

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

Cites work

• Addition and multiplication of sets
• Finite sets and Gödel's incompleteness theorems

Described by source

• A formalisation of finite automata using hereditarily finite sets

Cited in

(13)

• 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
• Two-Way Automata in Coq
• Hereditarily finite sets in constructive type theory
• Myhill-Nerode
• POSIX Lexing
• Presburger Automata
• Regular Sets
• Hotel Key Card
• Finite Automata HF
• Regex_Equivalence
• MSO_Regex_Equivalence

This page was built for software: Hereditarily Finite Sets