A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl).

Chunhan Wu, Xingyuan Zhang, Christian Urban

Browse the full ITP paper archive.