% $ 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