diff -r 31abe0e496bc -r 599239394c51 PhdThesisRealOne/LaTeXTemplates_masters-doctoral-thesis_v2/main.bbl --- a/PhdThesisRealOne/LaTeXTemplates_masters-doctoral-thesis_v2/main.bbl Thu Mar 24 20:59:43 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,197 +0,0 @@ -% $ 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