diff -r d68b9db4c9ec -r 26a5e640cdd7 PhdThesisRealOne/LaTeXTemplates_masters-doctoral-thesis_v2/main.bbl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/PhdThesisRealOne/LaTeXTemplates_masters-doctoral-thesis_v2/main.bbl Sun Mar 20 23:32:08 2022 +0000 @@ -0,0 +1,197 @@ +% $ biblatex auxiliary file $ +% $ biblatex bbl format version 2.9 $ +% Do not modify the above lines! +% +% This is an auxiliary file used by the 'biblatex' package. +% This file may safely be deleted. It will be recreated as +% required. +% +\begingroup +\makeatletter +\@ifundefined{ver@biblatex.sty} + {\@latex@error + {Missing 'biblatex' package} + {The bibliography requires the 'biblatex' package.} + \aftergroup\endinput} + {} +\endgroup + +\datalist[entry]{nyt/global//global/global} + \entry{Brzozowski1964}{article}{} + \name{author}{1}{}{% + {{hash=BJA}{% + family={Brzozowski}, + familyi={B\bibinitperiod}, + given={J.\bibnamedelima A.}, + giveni={J\bibinitperiod\bibinitdelim A\bibinitperiod}, + }}% + } + \strng{namehash}{BJA1} + \strng{fullhash}{BJA1} + \field{labelnamesource}{author} + \field{labeltitlesource}{title} + \field{labelyear}{1964} + \field{labeldatesource}{year} + \field{sortinit}{B} + \field{sortinithash}{B} + \field{number}{4} + \field{pages}{481\bibrangedash 494} + \field{title}{{D}erivatives of {R}egular {E}xpressions} + \field{volume}{11} + \field{journaltitle}{Journal of the {ACM}} + \field{year}{1964} + \endentry + + \entry{Coquand2012}{inproceedings}{} + \name{author}{2}{}{% + {{hash=CT}{% + family={Coquand}, + familyi={C\bibinitperiod}, + given={T.}, + giveni={T\bibinitperiod}, + }}% + {{hash=SV}{% + family={Siles}, + familyi={S\bibinitperiod}, + given={V.}, + giveni={V\bibinitperiod}, + }}% + } + \strng{namehash}{CTSV1} + \strng{fullhash}{CTSV1} + \field{labelnamesource}{author} + \field{labeltitlesource}{title} + \field{labelyear}{2011} + \field{labeldatesource}{year} + \field{sortinit}{C} + \field{sortinithash}{C} + \field{booktitle}{Proc.~of the 1st International Conference on Certified + Programs and Proofs (CPP)} + \field{pages}{119\bibrangedash 134} + \field{series}{LNCS} + \field{title}{{A} {D}ecision {P}rocedure for {R}egular {E}xpression + {E}quivalence in {T}ype {T}heory} + \field{volume}{7086} + \field{year}{2011} + \endentry + + \entry{Krauss2011}{article}{} + \name{author}{2}{}{% + {{hash=KA}{% + family={Krauss}, + familyi={K\bibinitperiod}, + given={A.}, + giveni={A\bibinitperiod}, + }}% + {{hash=NT}{% + family={Nipkow}, + familyi={N\bibinitperiod}, + given={T.}, + giveni={T\bibinitperiod}, + }}% + } + \strng{namehash}{KANT1} + \strng{fullhash}{KANT1} + \field{labelnamesource}{author} + \field{labeltitlesource}{title} + \field{labelyear}{2012} + \field{labeldatesource}{year} + \field{sortinit}{K} + \field{sortinithash}{K} + \field{pages}{95\bibrangedash 106} + \field{title}{{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and + {R}elation {A}lgebra} + \field{volume}{49} + \field{journaltitle}{Journal of Automated Reasoning} + \field{year}{2012} + \endentry + + \entry{Owens2008}{article}{} + \name{author}{2}{}{% + {{hash=OS}{% + family={Owens}, + familyi={O\bibinitperiod}, + given={S.}, + giveni={S\bibinitperiod}, + }}% + {{hash=SK}{% + family={Slind}, + familyi={S\bibinitperiod}, + given={K.}, + giveni={K\bibinitperiod}, + }}% + } + \strng{namehash}{OSSK1} + \strng{fullhash}{OSSK1} + \field{labelnamesource}{author} + \field{labeltitlesource}{title} + \field{labelyear}{2008} + \field{labeldatesource}{year} + \field{sortinit}{O} + \field{sortinithash}{O} + \field{number}{4} + \field{pages}{377\bibrangedash 409} + \field{title}{{A}dapting {F}unctional {P}rograms to {H}igher {O}rder + {L}ogic} + \field{volume}{21} + \field{journaltitle}{Higher-Order and Symbolic Computation} + \field{year}{2008} + \endentry + + \entry{RibeiroAgda2017}{inproceedings}{} + \name{author}{2}{}{% + {{hash=RR}{% + family={Ribeiro}, + familyi={R\bibinitperiod}, + given={Rodrigo}, + giveni={R\bibinitperiod}, + }}% + {{hash=BAD}{% + family={Bois}, + familyi={B\bibinitperiod}, + given={Andr\'{e}\bibnamedelima Du}, + giveni={A\bibinitperiod\bibinitdelim D\bibinitperiod}, + }}% + } + \list{publisher}{1}{% + {Association for Computing Machinery}% + } + \keyw{Certified algorithms, regular expressions, dependent types, + bit-codes} + \strng{namehash}{RRBAD1} + \strng{fullhash}{RRBAD1} + \field{labelnamesource}{author} + \field{labeltitlesource}{title} + \field{labelyear}{2017} + \field{labeldatesource}{year} + \field{sortinit}{R} + \field{sortinithash}{R} + \field{abstract}{% + We describe the formalization of a regular expression (RE) parsing + algorithm that produces a bit representation of its parse tree in the + dependently typed language Agda. The algorithm computes bit-codes using + Brzozowski derivatives and we prove that produced codes are equivalent to + parse trees ensuring soundness and completeness w.r.t an inductive RE + semantics. We include the certified algorithm in a tool developed by us, + named verigrep, for regular expression based search in the style of the well + known GNU grep. Practical experiments conducted with this tool are reported.% + } + \field{booktitle}{Proceedings of the 21st Brazilian Symposium on + Programming Languages} + \verb{doi} + \verb 10.1145/3125374.3125381 + \endverb + \field{isbn}{9781450353892} + \field{series}{SBLP 2017} + \field{title}{Certified Bit-Coded Regular Expression Parsing} + \verb{url} + \verb https://doi.org/10.1145/3125374.3125381 + \endverb + \list{location}{1}{% + {Fortaleza, CE, Brazil}% + } + \field{year}{2017} + \warn{\item Can't use 'location' + 'address'} + \endentry +\enddatalist +\endinput