|
456
|
1 |
% $ biblatex auxiliary file $
|
|
|
2 |
% $ biblatex bbl format version 2.9 $
|
|
|
3 |
% Do not modify the above lines!
|
|
|
4 |
%
|
|
|
5 |
% This is an auxiliary file used by the 'biblatex' package.
|
|
|
6 |
% This file may safely be deleted. It will be recreated as
|
|
|
7 |
% required.
|
|
|
8 |
%
|
|
|
9 |
\begingroup
|
|
|
10 |
\makeatletter
|
|
|
11 |
\@ifundefined{ver@biblatex.sty}
|
|
|
12 |
{\@latex@error
|
|
|
13 |
{Missing 'biblatex' package}
|
|
|
14 |
{The bibliography requires the 'biblatex' package.}
|
|
|
15 |
\aftergroup\endinput}
|
|
|
16 |
{}
|
|
|
17 |
\endgroup
|
|
|
18 |
|
|
|
19 |
\datalist[entry]{nyt/global//global/global}
|
|
|
20 |
\entry{Brzozowski1964}{article}{}
|
|
|
21 |
\name{author}{1}{}{%
|
|
|
22 |
{{hash=BJA}{%
|
|
|
23 |
family={Brzozowski},
|
|
|
24 |
familyi={B\bibinitperiod},
|
|
|
25 |
given={J.\bibnamedelima A.},
|
|
|
26 |
giveni={J\bibinitperiod\bibinitdelim A\bibinitperiod},
|
|
|
27 |
}}%
|
|
|
28 |
}
|
|
|
29 |
\strng{namehash}{BJA1}
|
|
|
30 |
\strng{fullhash}{BJA1}
|
|
|
31 |
\field{labelnamesource}{author}
|
|
|
32 |
\field{labeltitlesource}{title}
|
|
|
33 |
\field{labelyear}{1964}
|
|
|
34 |
\field{labeldatesource}{year}
|
|
|
35 |
\field{sortinit}{B}
|
|
|
36 |
\field{sortinithash}{B}
|
|
|
37 |
\field{number}{4}
|
|
|
38 |
\field{pages}{481\bibrangedash 494}
|
|
|
39 |
\field{title}{{D}erivatives of {R}egular {E}xpressions}
|
|
|
40 |
\field{volume}{11}
|
|
|
41 |
\field{journaltitle}{Journal of the {ACM}}
|
|
|
42 |
\field{year}{1964}
|
|
|
43 |
\endentry
|
|
|
44 |
|
|
|
45 |
\entry{Coquand2012}{inproceedings}{}
|
|
|
46 |
\name{author}{2}{}{%
|
|
|
47 |
{{hash=CT}{%
|
|
|
48 |
family={Coquand},
|
|
|
49 |
familyi={C\bibinitperiod},
|
|
|
50 |
given={T.},
|
|
|
51 |
giveni={T\bibinitperiod},
|
|
|
52 |
}}%
|
|
|
53 |
{{hash=SV}{%
|
|
|
54 |
family={Siles},
|
|
|
55 |
familyi={S\bibinitperiod},
|
|
|
56 |
given={V.},
|
|
|
57 |
giveni={V\bibinitperiod},
|
|
|
58 |
}}%
|
|
|
59 |
}
|
|
|
60 |
\strng{namehash}{CTSV1}
|
|
|
61 |
\strng{fullhash}{CTSV1}
|
|
|
62 |
\field{labelnamesource}{author}
|
|
|
63 |
\field{labeltitlesource}{title}
|
|
|
64 |
\field{labelyear}{2011}
|
|
|
65 |
\field{labeldatesource}{year}
|
|
|
66 |
\field{sortinit}{C}
|
|
|
67 |
\field{sortinithash}{C}
|
|
|
68 |
\field{booktitle}{Proc.~of the 1st International Conference on Certified
|
|
|
69 |
Programs and Proofs (CPP)}
|
|
|
70 |
\field{pages}{119\bibrangedash 134}
|
|
|
71 |
\field{series}{LNCS}
|
|
|
72 |
\field{title}{{A} {D}ecision {P}rocedure for {R}egular {E}xpression
|
|
|
73 |
{E}quivalence in {T}ype {T}heory}
|
|
|
74 |
\field{volume}{7086}
|
|
|
75 |
\field{year}{2011}
|
|
|
76 |
\endentry
|
|
|
77 |
|
|
|
78 |
\entry{Krauss2011}{article}{}
|
|
|
79 |
\name{author}{2}{}{%
|
|
|
80 |
{{hash=KA}{%
|
|
|
81 |
family={Krauss},
|
|
|
82 |
familyi={K\bibinitperiod},
|
|
|
83 |
given={A.},
|
|
|
84 |
giveni={A\bibinitperiod},
|
|
|
85 |
}}%
|
|
|
86 |
{{hash=NT}{%
|
|
|
87 |
family={Nipkow},
|
|
|
88 |
familyi={N\bibinitperiod},
|
|
|
89 |
given={T.},
|
|
|
90 |
giveni={T\bibinitperiod},
|
|
|
91 |
}}%
|
|
|
92 |
}
|
|
|
93 |
\strng{namehash}{KANT1}
|
|
|
94 |
\strng{fullhash}{KANT1}
|
|
|
95 |
\field{labelnamesource}{author}
|
|
|
96 |
\field{labeltitlesource}{title}
|
|
|
97 |
\field{labelyear}{2012}
|
|
|
98 |
\field{labeldatesource}{year}
|
|
|
99 |
\field{sortinit}{K}
|
|
|
100 |
\field{sortinithash}{K}
|
|
|
101 |
\field{pages}{95\bibrangedash 106}
|
|
|
102 |
\field{title}{{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and
|
|
|
103 |
{R}elation {A}lgebra}
|
|
|
104 |
\field{volume}{49}
|
|
|
105 |
\field{journaltitle}{Journal of Automated Reasoning}
|
|
|
106 |
\field{year}{2012}
|
|
|
107 |
\endentry
|
|
|
108 |
|
|
|
109 |
\entry{Owens2008}{article}{}
|
|
|
110 |
\name{author}{2}{}{%
|
|
|
111 |
{{hash=OS}{%
|
|
|
112 |
family={Owens},
|
|
|
113 |
familyi={O\bibinitperiod},
|
|
|
114 |
given={S.},
|
|
|
115 |
giveni={S\bibinitperiod},
|
|
|
116 |
}}%
|
|
|
117 |
{{hash=SK}{%
|
|
|
118 |
family={Slind},
|
|
|
119 |
familyi={S\bibinitperiod},
|
|
|
120 |
given={K.},
|
|
|
121 |
giveni={K\bibinitperiod},
|
|
|
122 |
}}%
|
|
|
123 |
}
|
|
|
124 |
\strng{namehash}{OSSK1}
|
|
|
125 |
\strng{fullhash}{OSSK1}
|
|
|
126 |
\field{labelnamesource}{author}
|
|
|
127 |
\field{labeltitlesource}{title}
|
|
|
128 |
\field{labelyear}{2008}
|
|
|
129 |
\field{labeldatesource}{year}
|
|
|
130 |
\field{sortinit}{O}
|
|
|
131 |
\field{sortinithash}{O}
|
|
|
132 |
\field{number}{4}
|
|
|
133 |
\field{pages}{377\bibrangedash 409}
|
|
|
134 |
\field{title}{{A}dapting {F}unctional {P}rograms to {H}igher {O}rder
|
|
|
135 |
{L}ogic}
|
|
|
136 |
\field{volume}{21}
|
|
|
137 |
\field{journaltitle}{Higher-Order and Symbolic Computation}
|
|
|
138 |
\field{year}{2008}
|
|
|
139 |
\endentry
|
|
|
140 |
|
|
|
141 |
\entry{RibeiroAgda2017}{inproceedings}{}
|
|
|
142 |
\name{author}{2}{}{%
|
|
|
143 |
{{hash=RR}{%
|
|
|
144 |
family={Ribeiro},
|
|
|
145 |
familyi={R\bibinitperiod},
|
|
|
146 |
given={Rodrigo},
|
|
|
147 |
giveni={R\bibinitperiod},
|
|
|
148 |
}}%
|
|
|
149 |
{{hash=BAD}{%
|
|
|
150 |
family={Bois},
|
|
|
151 |
familyi={B\bibinitperiod},
|
|
|
152 |
given={Andr\'{e}\bibnamedelima Du},
|
|
|
153 |
giveni={A\bibinitperiod\bibinitdelim D\bibinitperiod},
|
|
|
154 |
}}%
|
|
|
155 |
}
|
|
|
156 |
\list{publisher}{1}{%
|
|
|
157 |
{Association for Computing Machinery}%
|
|
|
158 |
}
|
|
|
159 |
\keyw{Certified algorithms, regular expressions, dependent types,
|
|
|
160 |
bit-codes}
|
|
|
161 |
\strng{namehash}{RRBAD1}
|
|
|
162 |
\strng{fullhash}{RRBAD1}
|
|
|
163 |
\field{labelnamesource}{author}
|
|
|
164 |
\field{labeltitlesource}{title}
|
|
|
165 |
\field{labelyear}{2017}
|
|
|
166 |
\field{labeldatesource}{year}
|
|
|
167 |
\field{sortinit}{R}
|
|
|
168 |
\field{sortinithash}{R}
|
|
|
169 |
\field{abstract}{%
|
|
|
170 |
We describe the formalization of a regular expression (RE) parsing
|
|
|
171 |
algorithm that produces a bit representation of its parse tree in the
|
|
|
172 |
dependently typed language Agda. The algorithm computes bit-codes using
|
|
|
173 |
Brzozowski derivatives and we prove that produced codes are equivalent to
|
|
|
174 |
parse trees ensuring soundness and completeness w.r.t an inductive RE
|
|
|
175 |
semantics. We include the certified algorithm in a tool developed by us,
|
|
|
176 |
named verigrep, for regular expression based search in the style of the well
|
|
|
177 |
known GNU grep. Practical experiments conducted with this tool are reported.%
|
|
|
178 |
}
|
|
|
179 |
\field{booktitle}{Proceedings of the 21st Brazilian Symposium on
|
|
|
180 |
Programming Languages}
|
|
|
181 |
\verb{doi}
|
|
|
182 |
\verb 10.1145/3125374.3125381
|
|
|
183 |
\endverb
|
|
|
184 |
\field{isbn}{9781450353892}
|
|
|
185 |
\field{series}{SBLP 2017}
|
|
|
186 |
\field{title}{Certified Bit-Coded Regular Expression Parsing}
|
|
|
187 |
\verb{url}
|
|
|
188 |
\verb https://doi.org/10.1145/3125374.3125381
|
|
|
189 |
\endverb
|
|
|
190 |
\list{location}{1}{%
|
|
|
191 |
{Fortaleza, CE, Brazil}%
|
|
|
192 |
}
|
|
|
193 |
\field{year}{2017}
|
|
|
194 |
\warn{\item Can't use 'location' + 'address'}
|
|
|
195 |
\endentry
|
|
|
196 |
\enddatalist
|
|
|
197 |
\endinput
|