


@TechReport{CrashCourse2014,
  author =       {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen},
  title =        {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular 
                  {E}xpressions as {T}ypes},
  institution =  {University of Copenhagen},
  year =         {2014},
  annote =       {draft report}
}

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

@inproceedings{Sulzmann2014b,
  author    = {M.~Sulzmann and P.~van Steenhoven},
  title     = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular
               {E}xpression {S}ubmatching},
  booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)},
  pages     = {174--191},
  year      = {2014},
  volume    = {8409},
  series =    {LNCS}
}

@book{Pierce2015,
  author = {B.~C.~Pierce and C.~Casinghino and M.~Gaboardi and
            M.~Greenberg and C.~Hri\c{t}cu and 
            V.~Sj\"{o}berg and B.~Yorgey},
  title = {{S}oftware {F}oundations},
  year = {2015},
  publisher = {Electronic textbook},
  note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}}
}

@Misc{Kuklewicz,
  author = 	 {C.~Kuklewicz},
  title = 	 {{R}egex {P}osix},
  howpublished = "\url{https://wiki.haskell.org/Regex_Posix}"
}

@article{Vansummeren2006,
  author = {S.~Vansummeren},
  title = {{T}ype {I}nference for {U}nique {P}attern {M}atching},
  year = {2006},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {28},
  number = {3},
  pages = {389--428}
}

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



