diff -r 56781ad291cf -r e00950ba4514 thys2/Journal/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thys2/Journal/document/root.bib Mon Nov 01 10:40:21 2021 +0000 @@ -0,0 +1,340 @@ +@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} +} +