Addressed Gerog "can't understand 'erase messes with structure'" comment
@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}}@InProceedings{NielsenHenglein2011, author = {L.~Nielsen and F.~Henglein}, title = {{B}it-{C}oded {R}egular {E}xpression {P}arsing}, booktitle = {Proc.~of the 5th International Conference on Language and Automata Theory and Applications (LATA)}, year = {2011}, pages = {402--413}, series = {LNCS}, volume = {6638}}@InProceedings{BjorklundMartensTimm2015, author = {H.~Bj\"{o}rklund and W.~Martens and T.~Timm}, title = {{E}fficient {I}ncremental {E}valuation of {S}uccinct {R}egular {E}xpressions}, booktitle = {Proc.~of the 24th ACM Conf.~on Information and Knowledge Management (CIKM)}, year = {2015}, pages = {1541--1550}}@Article{CountingSet2020,author = {L.~Turo\v{n}ov\'{a} and L.~Hol\'{\i}k and O.~Leng\'{a}l and O.~Saarikivi and M.~Veanes and T.~Vojnar},title = {{R}egex {M}atching with {C}ounting-{S}et {A}utomata},year = {2020},journal = {Proceedings of the ACM on Programming Languages (PACMPL)},publisher = {ACM},volume = {4},pages = {218:1--218:30}}@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},booktitle = {Proc.~of the 21st Brazilian Symposium on Programming Languages},pages = {4:1--4:8}}@INPROCEEDINGS{verbatim, author={D.~Egolf and S.~Lasser and K.~Fisher}, booktitle={2021 IEEE Security and Privacy Workshops (SPW)}, title={{V}erbatim: {A} {V}erified {L}exer {G}enerator}, year={2021}, volume={}, number={}, pages={92--100}}@inproceedings{verbatimpp, author = {D.~Egolf and S.~Lasser and K.~Fisher}, title = {{V}erbatim++: {V}erified, {O}ptimized, and {S}emantically {R}ich {L}exing with {D}derivatives}, booktitle = {Proc.~of the 11th {ACM} {SIGPLAN} Conference on Certified Programs and Proofs (CPP)}, pages = {27--39}, publisher = {{ACM}}, year = {2022}}@article{zipperparser, author = {P.~Darragh and M.~D.~Adams}, title = {{P}arsing with {Z}ippers ({F}unctional {P}earl)}, year = {2020}, issue_date = {August 2020}, publisher = {Association for Computing Machinery}, volume = {4}, journal = {Proc. ACM Program. Lang.}, number = {ICFP} }