%% This BibTeX bibliography file was created using BibDesk.%% https://bibdesk.sourceforge.io/%% Created for CS TAN at 2019-06-26 17:07:31 +0100 %% Saved with string encoding Unicode (UTF-8) @misc{SE16, Author = {StackStatus}, Date-Added = {2019-06-26 11:28:41 +0000}, Date-Modified = {2019-06-26 16:07:31 +0000}, Keywords = {ReDos Attack}, Month = {July}, Rating = {5}, Read = {1}, Title = {Stack Overflow Outage Postmortem}, Url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}, Year = {2016}, Bdsk-Url-1 = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}@article{HosoyaVouillonPierce2005, Author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce}, Journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, Number = 1, Pages = {46--90}, Title = {{R}egular {E}xpression {T}ypes for {XML}}, Volume = 27, Year = {2005}}@misc{POSIX, Note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}}, Title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition}, Year = {2004}}@inproceedings{AusafDyckhoffUrban2016, Author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, Booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)}, Pages = {69--86}, Series = {LNCS}, Title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)}, Volume = {9807}, Year = {2016}}@article{aduAFP16, Author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, Issn = {2150-914x}, Journal = {Archive of Formal Proofs}, Note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development}, Title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions}, Year = 2016}@techreport{CrashCourse2014, Annote = {draft report}, Author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen}, Institution = {University of Copenhagen}, Title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular {E}xpressions as {T}ypes}, Year = {2014}}@inproceedings{Sulzmann2014, Author = {M.~Sulzmann and K.~Lu}, Booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)}, Pages = {203--220}, Series = {LNCS}, Title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives}, Volume = {8475}, Year = {2014}}@inproceedings{Sulzmann2014b, Author = {M.~Sulzmann and P.~van Steenhoven}, Booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)}, Pages = {174--191}, Series = {LNCS}, Title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular {E}xpression {S}ubmatching}, Volume = {8409}, Year = {2014}}@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}, Note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}}, Publisher = {Electronic textbook}, Title = {{S}oftware {F}oundations}, Year = {2015}}@misc{Kuklewicz, Author = {C.~Kuklewicz}, Howpublished = {\url{https://wiki.haskell.org/Regex_Posix}}, Title = {{R}egex {P}osix}}@article{Vansummeren2006, Author = {S.~Vansummeren}, Journal = {ACM Transactions on Programming Languages and Systems}, Number = {3}, Pages = {389--428}, Title = {{T}ype {I}nference for {U}nique {P}attern {M}atching}, Volume = {28}, Year = {2006}}@inproceedings{Asperti12, Author = {A.~Asperti}, Booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)}, Pages = {283--298}, Series = {LNCS}, Title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence}, Volume = {7406}, Year = {2012}}@inproceedings{Frisch2004, Author = {A.~Frisch and L.~Cardelli}, Booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)}, Pages = {618--629}, Series = {LNCS}, Title = {{G}reedy {R}egular {E}xpression {M}atching}, Volume = {3142}, Year = {2004}}@article{Antimirov95, Author = {V.~Antimirov}, Journal = {Theoretical Computer Science}, Pages = {291--319}, Title = {{P}artial {D}erivatives of {R}egular {E}xpressions and {F}inite {A}utomata {C}onstructions}, Volume = {155}, Year = {1995}}@inproceedings{Nipkow98, Author = {T.~Nipkow}, Booktitle = {Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, Pages = {1--15}, Series = {LNCS}, Title = {{V}erified {L}exical {A}nalysis}, Volume = 1479, Year = 1998}@article{Brzozowski1964, Author = {J.~A.~Brzozowski}, Journal = {Journal of the {ACM}}, Number = {4}, Pages = {481--494}, Title = {{D}erivatives of {R}egular {E}xpressions}, Volume = {11}, Year = {1964}}@article{Leroy2009, Author = {X.~Leroy}, Journal = {Communications of the ACM}, Number = 7, Pages = {107--115}, Title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler}, Volume = 52, Year = 2009}@inproceedings{Paulson2015, Author = {L.~C.~Paulson}, Booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)}, Pages = {231--245}, Series = {LNAI}, Title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets}, Volume = {9195}, Year = {2015}}@article{Wu2014, Author = {C.~Wu and X.~Zhang and C.~Urban}, Journal = {Journal of Automatic Reasoning}, Number = {4}, Pages = {451--480}, Title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, Volume = {52}, Year = {2014}}@inproceedings{Regehr2011, Author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr}, Booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)}, Pages = {283--294}, Title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers}, Year = {2011}}@article{Norrish2014, Author = {A.~Barthwal and M.~Norrish}, Journal = {Journal of Computer and System Sciences}, Number = {2}, Pages = {346--362}, Title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}}, Volume = {80}, Year = {2014}}@article{Thompson1968, Author = {K.~Thompson}, Issue_Date = {June 1968}, Journal = {Communications of the ACM}, Number = {6}, Pages = {419--422}, Title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm}, Volume = {11}, Year = {1968}}@article{Owens2009, Author = {S.~Owens and J.~H.~Reppy and A.~Turon}, Journal = {Journal of Functinal Programming}, Number = {2}, Pages = {173--190}, Title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined}, Volume = {19}, Year = {2009}}@inproceedings{Sulzmann2015, Author = {M.~Sulzmann and P.~Thiemann}, Booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory and Applications (LATA)}, Pages = {275--286}, Series = {LNCS}, Title = {{D}erivatives for {R}egular {S}huffle {E}xpressions}, Volume = {8977}, Year = {2015}}@inproceedings{Chen2012, Author = {H.~Chen and S.~Yu}, Booktitle = {Proc.~in the International Workshop on Theoretical Computer Science (WTCS)}, Pages = {343--356}, Series = {LNCS}, Title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication}, Volume = {7160}, Year = {2012}}@article{Krauss2011, Author = {A.~Krauss and T.~Nipkow}, Journal = {Journal of Automated Reasoning}, Pages = {95--106}, Title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, Volume = 49, Year = 2012}@inproceedings{Traytel2015, Author = {D.~Traytel}, Booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)}, Pages = {487--503}, Series = {LIPIcs}, Title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}}, Volume = {41}, Year = {2015}}@inproceedings{Traytel2013, Author = {D.~Traytel and T.~Nipkow}, Booktitle = {Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)}, Pages = {3-12}, Title = {{A} {V}erified {D}ecision {P}rocedure for {MSO} on {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions}, Year = 2013}@inproceedings{Coquand2012, Author = {T.~Coquand and V.~Siles}, Booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)}, Pages = {119--134}, Series = {LNCS}, Title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory}, Volume = {7086}, Year = {2011}}@inproceedings{Almeidaetal10, Author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa}, Booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)}, Pages = {59-68}, Series = {LNCS}, Title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq}, Volume = {6482}, Year = {2010}}@article{Owens2008, Author = {S.~Owens and K.~Slind}, Journal = {Higher-Order and Symbolic Computation}, Number = {4}, Pages = {377--409}, Title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, Volume = {21}, Year = {2008}}@article{Owens2, Author = {S.~Owens and K.~Slind}, Bibsource = {dblp computer science bibliography, http://dblp.org}, Biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08}, Doi = {10.1007/s10990-008-9038-0}, Journal = {Higher-Order and Symbolic Computation}, Number = {4}, Pages = {377--409}, Timestamp = {Wed, 16 Dec 2009 13:51:02 +0100}, Title = {Adapting functional programs to higher order logic}, Url = {http://dx.doi.org/10.1007/s10990-008-9038-0}, Volume = {21}, Year = {2008}, Bdsk-Url-1 = {http://dx.doi.org/10.1007/s10990-008-9038-0}}@misc{PCRE, Title = {{PCRE - Perl Compatible Regular Expressions}}, Url = {http://www.pcre.org}, Bdsk-Url-1 = {http://www.pcre.org}}@inproceedings{OkuiSuzuki2010, Author = {S.~Okui and T.~Suzuki}, Booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)}, Pages = {231--240}, Series = {LNCS}, Title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions}, Volume = {6482}, Year = {2010}}@techreport{OkuiSuzukiTech, Author = {S.~Okui and T.~Suzuki}, Institution = {University of Aizu}, Title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions}, Year = {2013}}@inproceedings{Davis18, Author = {J.~C.~Davis and C.~.A.~Coghlan and F.~Servant and D.~Lee}, Booktitle = {Proc.~of the 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)}, Numpages = {11}, Pages = {246--256}, Title = {{T}he {I}mpact of {R}egular {E}xpression {D}enial of {S}ervice ({ReDoS}) in {P}ractice: {A}n {E}mpirical {S}tudy at the {E}cosystem {S}cale}, Year = {2018}}