--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Paper/document/root.bib Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,331 @@
+@inproceedings{Sulzmann2014,
+ author = {M.~Sulzmann and K.~Lu},
+ title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},
+ booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},
+ pages = {203--220},
+ year = {2014},
+ volume = {8475},
+ series = {LNCS}
+}
+
+@Misc{Kuklewicz,
+ author = {C.~Kuklewicz},
+ title = {{R}egex {P}osix},
+ howpublished = "\url{https://wiki.haskell.org/Regex_Posix}"
+}
+
+@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 (ITP)},
+ pages = {283--298},
+ year = {2012},
+ volume = {7406},
+ series = {LNCS}
+}
+
+@inproceedings{Frisch2004,
+ author = {A.~Frisch and L.~Cardelli},
+ title = {{G}reedy {R}egular {E}xpression {M}atching},
+ booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)},
+ pages = {618--629},
+ year = {2004},
+ volume = {3142},
+ series = {LNCS}
+}
+
+@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}
+}
+
+@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 (TPHOLs)},
+ series={LNCS},
+ volume=1479,
+ pages={1--15},
+ year=1998
+}
+
+@article{Brzozowski1964,
+ author = {J.~A.~Brzozowski},
+ title = {{D}erivatives of {R}egular {E}xpressions},
+ journal = {Journal of the {ACM}},
+ volume = {11},
+ number = {4},
+ pages = {481--494},
+ year = {1964}
+}
+
+@article{Leroy2009,
+ 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}
+}
+
+@InProceedings{Paulson2015,
+ author = {L.~C.~Paulson},
+ title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets},
+ booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)},
+ pages = {231--245},
+ year = {2015},
+ volume = {9195},
+ series = {LNAI}
+}
+
+@Article{Wu2014,
+ 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},
+ journal = {Journal of Automatic Reasoning},
+ year = {2014},
+ volume = {52},
+ number = {4},
+ pages = {451--480}
+}
+
+@InProceedings{Regehr2011,
+ author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr},
+ title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers},
+ pages = {283--294},
+ year = {2011},
+ booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and
+ Implementation (PLDI)}
+}
+
+@Article{Norrish2014,
+ author = {A.~Barthwal and M.~Norrish},
+ title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}},
+ journal = {Journal of Computer and System Sciences},
+ year = {2014},
+ volume = {80},
+ number = {2},
+ pages = {346--362}
+}
+
+@Article{Thompson1968,
+ author = {K.~Thompson},
+ title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm},
+ journal = {Communications of the ACM},
+ issue_date = {June 1968},
+ volume = {11},
+ number = {6},
+ year = {1968},
+ pages = {419--422}
+}
+
+@article{Owens2009,
+ author = {S.~Owens and J.~H.~Reppy and A.~Turon},
+ title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
+ journal = {Journal of Functinal Programming},
+ volume = {19},
+ number = {2},
+ pages = {173--190},
+ year = {2009}
+}
+
+@inproceedings{Sulzmann2015,
+ author = {M.~Sulzmann and P.~Thiemann},
+ title = {{D}erivatives for {R}egular {S}huffle {E}xpressions},
+ booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory
+ and Applications (LATA)},
+ pages = {275--286},
+ year = {2015},
+ volume = {8977},
+ series = {LNCS}
+}
+
+@inproceedings{Chen2012,
+ author = {H.~Chen and S.~Yu},
+ title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication},
+ booktitle = {Proc.~in the International Workshop on Theoretical
+ Computer Science (WTCS)},
+ pages = {343--356},
+ year = {2012},
+ volume = {7160},
+ series = {LNCS}
+}
+
+@article{Krauss2011,
+ 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,
+ pages={95--106},
+ year=2012
+}
+
+@InProceedings{Traytel2015,
+ author = {D.~Traytel},
+ title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}},
+ booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)},
+ pages = {487--503},
+ series = {LIPIcs},
+ year = {2015},
+ volume = {41}
+}
+
+@inproceedings{Traytel2013,
+ author={D.~Traytel and T.~Nipkow},
+ title={{A} {V}erified {D}ecision {P}rocedure for {MSO} on
+ {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions},
+ booktitle={Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)},
+ pages={3-12},
+ year=2013
+}
+
+@InProceedings{Coquand2012,
+ 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 (CPP)},
+ pages = {119--134},
+ year = {2011},
+ volume = {7086},
+ series = {LNCS}
+}
+
+@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 (CIAA)},
+ pages = {59-68},
+ year = {2010},
+ volume = {6482},
+ series = {LNCS}
+}
+
+@book{Michaelson,
+ title={An introduction to functional programming through lambda calculus},
+ author={Michaelson, Greg},
+ year={2011},
+ publisher={Courier Corporation}
+}
+
+@article{Owens2008,
+ 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}
+}
+
+
+@book{Velleman,
+ title={How to prove it: a structured approach},
+ author={Velleman, Daniel J},
+ year={2006},
+ publisher={Cambridge University Press}
+}
+
+@book{Jones,
+ title={Implementing functional languages:[a tutorial]},
+ author={Jones, Simon L Peyton and Lester, David R},
+ volume={124},
+ year={1992},
+ publisher={Prentice Hall Reading}
+}
+
+@article{Cardelli,
+ title={Type systems},
+ author={Cardelli, Luca},
+ journal={ACM Computing Surveys},
+ volume={28},
+ number={1},
+ pages={263--264},
+ year={1996}
+}
+
+@article{Morrisett,
+ author = {J. Gregory Morrisett and
+ Karl Crary and
+ Neal Glew and
+ David Walker},
+ title = {Stack-based typed assembly language},
+ journal = {J. Funct. Program.},
+ volume = {13},
+ number = {5},
+ pages = {957--959},
+ year = {2003},
+ url = {http://dx.doi.org/10.1017/S0956796802004446},
+ doi = {10.1017/S0956796802004446},
+ timestamp = {Fri, 19 Mar 2004 13:48:27 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/jfp/MorrisettCGW03},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@book{Nipkow,
+ title={Concrete Semantics: With Isabelle/HOL},
+ author={Nipkow, Tobias and Klein, Gerwin},
+ year={2014},
+ publisher={Springer}
+}
+
+@article{Dube,
+ author = {Danny Dub{\'{e}} and
+ Marc Feeley},
+ title = {Efficiently building a parse tree from a regular expression},
+ journal = {Acta Inf.},
+ volume = {37},
+ number = {2},
+ pages = {121--144},
+ year = {2000},
+ url = {http://link.springer.de/link/service/journals/00236/bibs/0037002/00370121.htm},
+ timestamp = {Tue, 25 Nov 2003 14:51:21 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/acta/DubeF00},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@article{Morrisett2,
+ author = {J. Gregory Morrisett and
+ David Walker and
+ Karl Crary and
+ Neal Glew},
+ title = {From system {F} to typed assembly language},
+ journal = {{ACM} Trans. Program. Lang. Syst.},
+ volume = {21},
+ number = {3},
+ pages = {527--568},
+ year = {1999},
+ url = {http://doi.acm.org/10.1145/319301.319345},
+ doi = {10.1145/319301.319345},
+ timestamp = {Wed, 26 Nov 2003 14:26:46 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/MorrisettWCG99},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@article{Owens2,
+ author = {Scott Owens and
+ Konrad Slind},
+ title = {Adapting functional programs to higher order logic},
+ journal = {Higher-Order and Symbolic Computation},
+ volume = {21},
+ number = {4},
+ pages = {377--409},
+ year = {2008},
+ url = {http://dx.doi.org/10.1007/s10990-008-9038-0},
+ doi = {10.1007/s10990-008-9038-0},
+ timestamp = {Wed, 16 Dec 2009 13:51:02 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@misc{PCRE,
+ title = "{PCRE - Perl Compatible Regular Expressions}",
+ url = {http://www.pcre.org},
+}
+
+
+