@InProceedings{CoquandSiles12,

  author =       {T.~Coquand and V.~Siles},

  title =        {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},

  booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs},

  pages =     {119--134},

  year =      {2011},

  volume =    {7086},

  series =    {LNCS}

}

@InProceedings{Asperti12,

  author =       {A.~Asperti},

  title =        {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},

  booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},

  pages =     {283--298},

  year =      {2012},

  volume =    {7406},

  series =    {LNCS}

}

@InProceedings{LammichTuerk12,

  author =       {P.~Lammich and T.~Tuerk},

  title =        {{A}pplying {D}ata {R}efinement for {M}onadic {P}rograms to {H}opcroft's {A}lgorithm},

  booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},

  year =      {2012},

  volume =    {7406},

  series =    {LNCS},

  pages = {166--182}

}

@PhdThesis{Braibant12,

  author =       {T.~Braibant},

  title =        {{K}leene {A}lgebras, {R}ewriting {M}odulo {AC}, and {C}ircuits in {C}oq},

  school =       {University of Grenoble},

  year =         {2012}

}

@incollection{Nipkow11,

  author =       {T.~Nipkow},

  title =        {{G}auss-{J}ordan {E}limination for {M}atrices {R}epresented as {F}unctions},

  booktitle =    {The Archive of Formal Proofs},

  editor =       {G.~Klein and T.~Nipkow and L.~Paulson},

  publisher =    {\url{http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml}},

  year =         2011,

  note =         {Formal proof development},

  ISSN =         {2150-914x}

}

@Article{Haines69,

  author = 	 {L.~H.~Haines},

  title = 	 {{O}n {F}ree {M}onoids {P}artially {O}rdered by {E}mbedding},

  journal = 	 {Journal of Combinatorial Theory},

  year = 	 {1969},

  volume = 	 {6},

  pages = 	 {94--98}

}

@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 of 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/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}

}

@article{KraussNipkow11,

  author = 	 {A.~Krauss and T.~Nipkow},

  title = 	 {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},

  journal = {Journal of Automated Reasoning},

  volume = 49,

  number = {1},

  year = 	 {2012},

  pages = {95--106}

}

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

 number = {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{Okhotin04,

  author =	"A.~Okhotin",

  title =	"{B}oolean {G}rammars",

  journal =	"Information and Computation",

  pages =	"19--48",

  year = 	"2004",

  number =	"1",

  volume =	"194"

}

@Article{KountouriotisNR09,

  title =	"{W}ell-founded {S}emantics for {B}oolean {G}rammars",

  author =	"V.~Kountouriotis and C.~Nomikos and P.~Rondogiannis",

  journal =	"Information and Computation",

  year = 	"2009",

  number =	"9",

  volume =	"207",

  pages     =   "945--967"

}

@article{Leroy09,

  author =      {X.~Leroy},

  title =       {{F}ormal {V}erification of a {R}ealistic {C}ompiler},

  journal =     {Communications of the ACM},

  year =        {2009},

  volume =      {52},

  number =      {7},

  pages =       {107--115}

}

@Unpublished{Might11,

  title =	"{Y}acc is {D}ead",

  author =	"M.~Might and D.~Darais",

  note  =       "To appear in {\it Proc.~of the 16th ACM International Conference on 

                 Functional Programming (ICFP)}",

  year =        "2011"

}

@InProceedings{Ford04,

  author =	"B.~Ford",

  title =	"{P}arsing {E}xpression {G}rammars: {A} {R}ecognition-{B}ased

		 {S}yntactic {F}oundation",

  booktitle =	"Proc.~of the 31st ACM Symposium on Principles of Programming Languages (POPL)",

  year = 	"2004",

  pages =	"111--122"

}

@InProceedings{Ford02,

  author =	"B.~Ford",

  title =	"{P}ackrat {P}arsing: : {S}imple, {P}owerful, {L}azy, {L}inear {T}ime,

                 ({F}unctional {P}earl)",

  booktitle =	"Proc.~of the 7th ACM International Conference on Functional Programming (ICFP)",

  year = 	"2002",

  pages  =      "36--47"

}

@InProceedings{WarthDM08,

  title =	"{P}ackrat {P}arsers {C}an {S}upport {L}eft {R}ecursion",

  author =	"A.~Warth and J.~R.~Douglass and T.~D.~Millstein",

  booktitle =	"Proc. of the {ACM} Symposium on

		 Partial Evaluation and Semantics-based Program

		 Manipulation (PEPM)",

  year = 	"2008",

  pages =	"103--110"

}

@Article{Earley70,

  author =	"J.~Earley",

  title =	"{A}n {E}fficient {C}ontext-{F}ree {P}arsing {A}lgorithm",

  journal =	"Communications of the ACM",

  volume =	"13",

  number =	"2",

  pages =       "94--102",

  year = 	"1970"

}

@Article{AycHor02,

  author =	"J.~Aycock and R.~N.~Horspool",

  title =	"{P}ractical {E}arley {P}arsing",

  journal =	"The Computer Journal",

  volume =	"45",

  number =      "6",

  pages =       "620--630",

  year = 	"2002",

}