ecp/root.bib
changeset 22 feffec3af1a1
parent 17 3241b1e71633
child 24 bffa240d5b7a
--- a/ecp/root.bib	Wed Jun 26 12:44:08 2019 +0100
+++ b/ecp/root.bib	Wed Jun 26 16:06:58 2019 +0100
@@ -1,350 +1,318 @@
-@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}}
-}
-
+%% This BibTeX bibliography file was created using BibDesk.
+%% https://bibdesk.sourceforge.io/
 
-@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}
-}
+%% Created for CS TAN at 2019-06-26 12:42:11 +0100 
 
 
-@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},
-}
+%% Saved with string encoding Unicode (UTF-8) 
 
 
 
-@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}
-}
+@url{SE16,
+	Author = {StackStatus},
+	Date-Added = {2019-06-26 11:28:41 +0000},
+	Date-Modified = {2019-06-26 11:42:11 +0000},
+	Keywords = {ReDos Attack},
+	Month = {07},
+	Rating = {5},
+	Read = {1},
+	Title = {Stack Overflow Outage Postmortem},
+	Url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016},
+	Urldate = {2016.7.20},
+	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}}
 
-@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}
-}
+@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},
- 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},
- booktitle = {Proc.~of the 26th ACM Joint Meeting on European Software Engineering
-              Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)},
- year = {2018},
- pages = {246--256},
- numpages = {11}
-}
\ No newline at end of file
+	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}}