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