@article{Gasarch09, author = {S.~A.~Fenner and W.~I.~Gasarch and B.~Postow}, title = {{T}he {C}omplexity of {F}inding {SUBSEQ(A)}}, journal = {Theory Computing Systems}, volume = {45}, number = {3}, year = {2009}, pages = {577-612}}@Book{Shallit08, author = {J.~Shallit}, title = {{A} {S}econd {C}ourse in {F}ormal {L}anguages and {A}utomata {T}heory}, publisher = {Cambridge University Press}, year = {2008}}@Unpublished{Rosenberg06, author = {A.~L.~Rosenberg}, title = {{A} {B}ig {I}deas {A}pproach to the {T}heory of {C}omputation}, note = {Course notes for CMPSCI 401 at the University of Massachusetts}, year = {2006}}@incollection{myhillnerodeafp11, author = {C.~Wu and X.~Zhang and C.~Urban}, title = {{T}he {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, booktitle = {The Archive of Formal Proofs}, editor = {G.~Klein and T.~Nipkow and L.~Paulson}, publisher = {\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}}, month = Aug, year = 2011, note = {Formal proof development}, ISSN = {2150-914x}}@PhdThesis{Haftmann09, author = {F.~Haftmann}, title = {{C}ode {G}eneration from {S}pecifications in {H}igher-{O}rder {L}ogic}, school = {Technical University of Munich}, year = {2009}}@article{Harper99, author = {R.~Harper}, title = {{P}roof-{D}irected {D}ebugging}, journal = {Journal of Functional Programming}, volume = {9}, number = {4}, year = {1999}, pages = {463-469}}@article{Yi06, author = {K.~Yi}, title = {{E}ducational {P}earl: `{P}roof-{D}irected {D}ebugging' {R}evisited for a {F}irst-{O}rder {V}ersion}, journal = {Journal of Functional Programming}, volume = {16}, number = {6}, year = {2006}, pages = {663-670}}@Manual{PittsHOL4, title = {{S}yntax and {S}emantics}, author = {A.~M.~Pitts}, note = {Part of the documentation for the HOL4 system.}}@article{OwensReppyTuron09, author = {S.~Owens and J.~Reppy and A.~Turon}, title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined}, journal = {Journal of Functional Programming}, volume = 19, number = {2}, year = 2009, pages = {173--190}}@Unpublished{KraussNipkow11, author = {A.~Krauss and T.~Nipkow}, title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, note = {To appear in Journal of Automated Reasoning}, year = {2011}}@Book{Kozen97, author = {D.~Kozen}, title = {{A}utomata and {C}omputability}, publisher = {Springer Verlag}, year = {1997}}@InProceedings{Almeidaetal10, author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa}, title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq}, booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata}, pages = {59-68}, year = {2010}, volume = {6482}, series = {LNCS}}@incollection{Constable00, author = {R.~L.~Constable and P.~B.~Jackson and P.~Naumov and J.~C.~Uribe}, title = {{C}onstructively {F}ormalizing {A}utomata {T}heory}, booktitle = {Proof, Language, and Interaction}, year = {2000}, publisher = {MIT Press}, pages = {213-238}}@techreport{Filliatre97, author = {J.-C. Filli\^atre}, institution = {LIP - ENS Lyon}, number = {97--04}, title = {{F}inite {A}utomata {T}heory in {C}oq: {A} {C}onstructive {P}roof of {K}leene's {T}heorem}, type = {Research Report}, year = {1997}}@article{OwensSlind08, author = {S.~Owens and K.~Slind}, title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, journal = {Higher-Order and Symbolic Computation}, volume = {21}, number = {4}, year = {2008}, pages = {377--409}}@article{Brzozowski64, author = {J.~A.~Brzozowski}, title = {{D}erivatives of {R}egular {E}xpressions}, journal = {Journal of the ACM}, volume = {11}, issue = {4}, year = {1964}, pages = {481--494}, publisher = {ACM}} @inproceedings{Nipkow98, author={T.~Nipkow}, title={{V}erified {L}exical {A}nalysis}, booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics}, series={LNCS}, volume=1479, pages={1--15}, year=1998}@inproceedings{BerghoferNipkow00, author={S.~Berghofer and T.~Nipkow}, title={{E}xecuting {H}igher {O}rder {L}ogic}, booktitle={Proc.~of the International Workshop on Types for Proofs and Programs}, year=2002, series={LNCS}, volume=2277, pages="24--40"}@book{HopcroftUllman69, author = {J.~E.~Hopcroft and J.~D.~Ullman}, title = {{F}ormal {L}anguages and {T}heir {R}elation to {A}utomata}, publisher = {Addison-Wesley}, year = {1969}}@inproceedings{BerghoferReiter09, author = {S.~Berghofer and M.~Reiter}, title = {{F}ormalizing the {L}ogic-{A}utomaton {C}onnection}, booktitle = {Proc.~of the 22nd International Conference on Theorem Proving in Higher Order Logics}, year = {2009}, pages = {147-163}, series = {LNCS}, volume = {5674}}@Article{Church40, author = {A.~Church}, title = {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes}, journal = {Journal of Symbolic Logic}, year = {1940}, volume = {5}, number = {2}, pages = {56--68}}@ARTICLE{Antimirov95, author = {V.~Antimirov}, title = {{P}artial {D}erivatives of {R}egular {E}xpressions and {F}inite {A}utomata {C}onstructions}, journal = {Theoretical Computer Science}, year = {1995}, volume = {155}, pages = {291--319}}@ARTICLE{Brzozowski10, author = {J.~A.~Brzozowski}, title = {{Q}uotient {C}omplexity of {R}egular {L}anguages}, journal = {Journal of Automata, Languages and Combinatorics}, volume = {15}, number = {1/2}, pages = {71--89}, year = 2010} @book{Sakarovitch09, author = {J.~Sakarovitch}, title = {{E}lements of {A}utomata {T}heory}, publisher = {Cambridge University Press}, year = {2009}}@inproceedings{WuZhangUrban11, author = {C.~Wu and X.~Zhang and C.~Urban}, title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions ({P}roof {P}earl)}, booktitle = {Proc.~of the 2nd International Conference on Interactive Theorem Proving}, year = {2011}, pages = {341--356}, series = {LNCS}, volume = {6898}}@Article{Okhotin/04a, author = "A. Okhotin", title = "Boolean {G}rammars", journal = "Inf.~Comput.", pages = "19--48", year = "2004", number = "1", volume = "194", keywords = "context-free grammar, intersection, complement, language equation, parsing, conjunctive grammar, trellis automaton, cellular automaton", abstract = "A new generalization of context-free grammars is introduced: Boolean grammars allow the use of all set-theoretic operations as an integral part of the formalism of rules. Rigorous semantics for these grammars is defined by language equations in a way that allows to generalize some techniques from the theory of context-free grammars, including Chomsky normal form, Cocke-Kasami-Younger cubic-time recognition algorithm and some limited extension of the notion of a parse tree, which together allow to conjecture practical applicability of the new concept. (Copyright 2004 ScienceDirect)", editor = "Albert R. Meyer", publisher = "Elsevier B.V.", address = "Orlando-Amsterdam-Tokyo-Singapore", URL = "http://dx.doi.org/10.1016/j.ic.2004.03.006", cdate = "2004-12-21", mdate = "2005-08-18",}@Article{journals/iandc/KountouriotisNR09, title = "{W}ell-founded {S}emantics for Boolean {G}rammars", author = "V. Kountouriotis and C. Nomikos and P. Rondogiannis", journal = "Inf. Comput", year = "2009", number = "9", volume = "207", bibdate = "2009-09-08", bibsource = "DBLP, http://dblp.uni-trier.de/db/journals/iandc/iandc207.html#KountouriotisNR09", pages = "945--967", URL = "http://dx.doi.org/10.1016/j.ic.2009.05.002",}@Article{journals/corr/abs-1010-5023, title = "Yacc is {D}ead", author = "M. Might and D. Darais", journal = "CoRR", year = "2010", volume = "abs/1010.5023", note = "informal publication", bibdate = "2010-11-03", bibsource = "DBLP, http://dblp.uni-trier.de/db/journals/corr/corr1010.html#abs-1010-5023", URL = "http://arxiv.org/abs/1010.5023",}@InProceedings{Ford04a, author = "B. Ford", title = "Parsing {E}xpression {G}rammars: {A} {R}ecognition-based {S}yntactic {F}oundation", booktitle = "POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages", year = "2004", ISBN = "1-58113-729-X", pages = "111--122", location = "Venice, Italy", doi = "10.1145/964001.964011", URL = "http://pdos.csail.mit.edu/~baford/packrat/popl04/peg-popl04.pdf", publisher = "ACM", address = "New York, NY, USA", keywords = "peg parsing cclit", doi-url = "http://dx.doi.org/10.1145/964001.964011",}@InProceedings{Ford02b, author = "B. Ford", title = "{Packrat Parsing: a Practical Linear-Time Algorithm with Backtracking}", booktitle = "ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming", year = "2002", school = "Massachusetts Institute of Technology", URL = "http://pdos.csail.mit.edu/~baford/packrat/thesis/ http://pdos.csail.mit.edu/~baford/packrat/thesis/thesis.pdf", keywords = "packrat parsing cclit",}@InProceedings{conf/pepm/WarthDM08, title = "{Packrat Parsers Can Support Left Recursion}", author = "A. Warth and J. R. Douglass and T. D. Millstein", bibdate = "2008-04-04", bibsource = "DBLP, http://dblp.uni-trier.de/db/conf/pepm/pepm2008.html#WarthDM08", booktitle = "PEPM", booktitle = "Proceedings of the 2008 {ACM} {SIGPLAN} Symposium on Partial Evaluation and Semantics-based Program Manipulation, {PEPM} 2008, San Francisco, California, {USA}, January 7-8, 2008", publisher = "ACM", year = "2008", editor = "Robert Gl{\"u}ck and Oege de Moor", ISBN = "978-1-59593-977-7", pages = "103--110", URL = "http://doi.acm.org/10.1145/1328408.1328424",}@Article{Earley70, author = "J. Earley", title = "{An Efficient Context-Free Parsing Algorithm}", journal = "Communications of the ACM (CACM)", volume = "13", number = "2", month = feb, year = "1970", keywords = "parallel parsing, syntax analysis, parsing, context-free grammar, compilers, computational complexity, CACM,",}@Article{AycHor02, author = "Aycock and Horspool", title = "{Practical Earley Parsing}", journal = "COMPJ: The Computer Journal", volume = "45", year = "2002",}