@article{HosoyaVouillonPierce2005,

  author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce},

  title = {{R}egular {E}xpression {T}ypes for {XML}},

  journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},

  year = {2005},

  volume = 27,

  number = 1,

  pages = {46--90}

}

@Misc{POSIX,

  title =     {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition},

  year =      {2004},

  note =    {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}}

}

@InProceedings{AusafDyckhoffUrban2016,

  author =   {F.~Ausaf and R.~Dyckhoff and C.~Urban},

  title = 	 {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},

  year = 	 {2016},

  booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},

  volume = 	 {9807},

  series = 	 {LNCS},

  pages =        {69--86}

}

@article{aduAFP16,

  author =   {F.~Ausaf and R.~Dyckhoff and C.~Urban},

  title =    {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},

  journal =  {Archive of Formal Proofs},

  year =     2016,

  note =     {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development},

  ISSN =     {2150-914x}

}

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

}

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

}

@article{Owens2,

  author    = {S.~Owens and K.~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},

}

@InProceedings{OkuiSuzuki2010,

  author =       {S.~Okui and T.~Suzuki},

  title =        {{D}isambiguation in {R}egular {E}xpression {M}atching via

                  {P}osition {A}utomata with {A}ugmented {T}ransitions},

  booktitle = {Proc.~of the 15th International Conference on Implementation

                  and Application of Automata (CIAA)},

  year =      {2010},

  volume =    {6482},

  series =    {LNCS},

  pages =     {231--240}

}

@TechReport{OkuiSuzukiTech,

  author =       {S.~Okui and T.~Suzuki},

  title =        {{D}isambiguation in {R}egular {E}xpression {M}atching via

                  {P}osition {A}utomata with {A}ugmented {T}ransitions},

  institution =  {University of Aizu},

  year =         {2013}

}

@inproceedings{RibeiroAgda2017,

author = {R.~Ribeiro and A.~Du Bois},

title = {{C}ertified {B}it-{C}oded {R}egular {E}xpression {P}arsing},

year = {2017},

publisher = {Association for Computing Machinery},

address = {New York, NY, USA},

booktitle = {Proc.~of the 21st Brazilian Symposium on Programming Languages},

articleno = {4},

numpages = {8}

}