Email Gateway (Aug 18 2022 at 18:31): Email Gateway (Aug 18 2022 at 18:31):From: Gerwin Klein <gerwin.klein@nicta.com.au>
All entries in the AFP are now available for Isabelle 2011-1 at [http://afp.sf.net]
In addition, the following entry has become available from the front page:
The Myhill-Nerode Theorem Based on Regular Expressions
by Chunhan Wu, Xingyuan Zhang, Christian Urban
[http://afp.sourceforge.net/entries/Myhill-Nerode.shtml]
Abstract
There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages. Most details of the theories are described in our ITP 2011 paper.
The following entries have new change-history items since the last release:
[http://afp.sourceforge.net/entries/Presburger-Automata.shtml]
[http://afp.sourceforge.net/entries/FileRefinement.shtml]
[http://afp.sourceforge.net/entries/Stream-Fusion.shtml]
[http://afp.sourceforge.net/entries/Locally-Nameless-Sigma.shtml]
Have fun!
Gerwin
Email Gateway (Aug 18 2022 at 18:31):From: Gerwin Klein <gerwin.klein@nicta.com.au>
No idea how I managed to mangle that so badly. The entries that actually have new change-history items since the last release are:
[http://afp.sourceforge.net/entries/Collections.shtml]
[http://afp.sourceforge.net/entries/Coinductive.shtml]
[http://afp.sourceforge.net/entries/JinjaThreads.shtml]
[http://afp.sourceforge.net/entries/Marriage.shtml]
Cheers,
Gerwin
Last updated: May 06 2024 at 20:16 UTC