--- /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