@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.~Kraus 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}+
−
}+
−
+
−
+
−
@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 = {J.~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{Brozowski10,+
−
  author = {J.~Brozowski},+
−
  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},+
−
  booktitle = {Proc.~of the 2nd 1st Conference on Interactive Theorem Proving},+
−
  year      = {2011},+
−
  pages     = {???},+
−
  series    = {LNCS},+
−
  volume    = {???}+
−
}+
−