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