
@inproceedings{Berghofer03,
  author    = {S.~Berghofer},
  title     = {{A} {C}onstructive {P}roof of {H}igman's {L}emma in {I}sabelle},
  booktitle = {In Proc. of the Workshop on Types},
  year      = {2003},
  pages     = {66--82},
  series    = {LNCS},
  volume    = {3085}
}

@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",
}

