Email Gateway (Aug 18 2022 at 10:49): Email Gateway (Aug 18 2022 at 10:49):From: Tim Newsham <newsham@lava.net>
Are there any existing proofs about grammars in the libraries or proof
archives? I would like to be able to prove that some parsing code accepts
strings if and only if they are in some context free language specified by
a context free grammar (or possibly even a regular language and a
regular expression).
Tim Newsham
http://www.thenewsh.com/~newsham/
Email Gateway (Aug 18 2022 at 10:51):From: Yasuhiko Minamide <minamide@score.cs.tsukuba.ac.jp>
Recently, I verfied several decision procedures on context-free grammars.
You can find my proof scripts in the following URL.
http://www.score.cs.tsukuba.ac.jp/~minamide/cfgv/
The work will be presented in TPHOLs 2007 in the next week.
Yasuhiko Minamide
Email Gateway (Aug 18 2022 at 10:51):From: Tobias Nipkow <nipkow@in.tum.de>
For automata and regular expressions see the AFP entry
http://afp.sourceforge.net/entries/Functional-Automata.shtml
Tobias
Last updated: May 03 2024 at 12:27 UTC