diff -r 12e9aa68d5db -r 4190df6f4488 prio/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/document/root.bib	Tue Jan 24 00:20:09 2012 +0000
@@ -0,0 +1,111 @@
+@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}
+}
\ No newline at end of file