%PDF-1.5
%
1 0 obj
<<
/Metadata 2 0 R
/Outlines 3 0 R
/Pages 4 0 R
/Type /Catalog
>>
endobj
5 0 obj
<<
/Author <4A616E2D4F6C69766572204B61697365722C2042657461205A696C69616E692C20526F6262657274204B726562626572732C2059616E6E2052E96769732D4769616E61732C20616E6420446572656B20447265796572>
/CreationDate (D:20180712104000-03'00')
/Creator (LaTeX with acmart 2018/04/14 v1.53 Typesetting articles for the Association for Computing Machinery and hyperref 2018/02/06 v6.86b Hypertext links for LaTeX)
/Keywords (Theorem Proving, Tactic Languages, Metaprogramming, Dependent Types, Coq)
/ModDate (D:20180712104000-03'00')
/PTEX.Fullbanner (This is pdfTeX, Version 3.14159265-2.6-1.40.18 \(TeX Live 2017/Debian\) kpathsea version 6.2.3)
/Producer (pdfTeX-1.40.18)
/Subject (- Theory of computation -> Type theory; Proof theory; )
/Title (Mtac2: Typed Tactics for Backward Reasoning in Coq)
>>
endobj
2 0 obj
<<
/Length 1956
/Subtype /XML
/Type /Metadata
>>
stream
GPL Ghostscript 9.21
Theorem Proving, Tactic Languages, Metaprogramming, Dependent Types, Coq
2018-07-28T12:16:02+02:00
2018-07-28T12:16:02+02:00
LaTeX with acmart 2018/04/14 v1.53 Typesetting articles for the Association for Computing Machinery and hyperref 2018/02/06 v6.86b Hypertext links for LaTeX
Mtac2: Typed Tactics for Backward Reasoning in CoqJan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann R�gis-Gianas, and Derek Dreyer- Theory of computation -> Type theory; Proof theory;
endstream
endobj
3 0 obj
<<
/Count 24
/First 6 0 R
/Last 7 0 R
/Type /Outlines
>>
endobj
4 0 obj
<<
/Count 32
/Kids [8 0 R 9 0 R 10 0 R 11 0 R 12 0 R 13 0 R 14 0 R 15 0 R 16 0 R 17 0 R
18 0 R 19 0 R 20 0 R 21 0 R 22 0 R 23 0 R 24 0 R 25 0 R 26 0 R 27 0 R
28 0 R 29 0 R 30 0 R 31 0 R 32 0 R 33 0 R 34 0 R 35 0 R 36 0 R 37 0 R
38 0 R 39 0 R]
/Type /Pages
>>
endobj
6 0 obj
<<
/Dest [9 0 R /Fit]
/Next 40 0 R
/Parent 3 0 R
/Title (Abstract)
>>
endobj
7 0 obj
<<
/Dest [38 0 R /Fit]
/Parent 3 0 R
/Prev 41 0 R
/Title (References)
>>
endobj
8 0 obj
<<
/Contents 42 0 R
/Type /Page
/Resources <<
/Font <<
/F1 43 0 R
>>
/XObject <<
/Xf1 44 0 R
>>
>>
/Annots [45 0 R 46 0 R]
/Parent 4 0 R
/MediaBox [0 0 595 842]
>>
endobj
9 0 obj
<<
/Annots [47 0 R 48 0 R 49 0 R 50 0 R 51 0 R]
/Contents [52 0 R 53 0 R 54 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 55 0 R
/Font 56 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi0 57 0 R
>>
>>
/Type /Page
>>
endobj
10 0 obj
<<
/Annots [58 0 R 59 0 R 60 0 R 61 0 R 62 0 R 63 0 R 64 0 R 65 0 R 66 0 R 67 0 R
68 0 R]
/Contents [69 0 R 70 0 R 71 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 72 0 R
/Font 73 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi1 74 0 R
>>
>>
/Type /Page
>>
endobj
11 0 obj
<<
/Annots [75 0 R 76 0 R 77 0 R 78 0 R 79 0 R 80 0 R 81 0 R 82 0 R 83 0 R]
/Contents [84 0 R 85 0 R 86 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 87 0 R
/Font 88 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi2 89 0 R
>>
>>
/Type /Page
>>
endobj
12 0 obj
<<
/Annots [90 0 R 91 0 R 92 0 R]
/Contents [93 0 R 94 0 R 95 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 96 0 R
/Font 97 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi3 98 0 R
>>
>>
/Type /Page
>>
endobj
13 0 obj
<<
/Annots [99 0 R 100 0 R 101 0 R 102 0 R]
/Contents [103 0 R 104 0 R 105 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 106 0 R
/Font 107 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi4 108 0 R
>>
>>
/Type /Page
>>
endobj
14 0 obj
<<
/Annots [109 0 R 110 0 R 111 0 R 112 0 R 113 0 R 114 0 R 115 0 R 116 0 R 117 0 R 118 0 R
119 0 R]
/Contents [120 0 R 121 0 R 122 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 123 0 R
/Font 124 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi5 125 0 R
>>
>>
/Type /Page
>>
endobj
15 0 obj
<<
/Annots [126 0 R 127 0 R 128 0 R 129 0 R]
/Contents [130 0 R 131 0 R 132 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 133 0 R
/Font 134 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi6 135 0 R
>>
>>
/Type /Page
>>
endobj
16 0 obj
<<
/Annots [136 0 R 137 0 R 138 0 R 139 0 R 140 0 R 141 0 R]
/Contents [142 0 R 143 0 R 144 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 145 0 R
/Font 146 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi7 147 0 R
>>
>>
/Type /Page
>>
endobj
17 0 obj
<<
/Annots [148 0 R]
/Contents [149 0 R 150 0 R 151 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 152 0 R
/Font 153 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi8 154 0 R
>>
>>
/Type /Page
>>
endobj
18 0 obj
<<
/Annots [155 0 R 156 0 R 157 0 R 158 0 R 159 0 R]
/Contents [160 0 R 161 0 R 162 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 163 0 R
/Font 164 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi9 165 0 R
>>
>>
/Type /Page
>>
endobj
19 0 obj
<<
/Annots [166 0 R 167 0 R 168 0 R 169 0 R 170 0 R 171 0 R 172 0 R 173 0 R 174 0 R]
/Contents [175 0 R 176 0 R 177 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 178 0 R
/Font 179 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi10 180 0 R
>>
>>
/Type /Page
>>
endobj
20 0 obj
<<
/Annots [181 0 R 182 0 R 183 0 R 184 0 R 185 0 R 186 0 R 187 0 R 188 0 R]
/Contents [189 0 R 190 0 R 191 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 192 0 R
/Font 193 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi11 194 0 R
>>
>>
/Type /Page
>>
endobj
21 0 obj
<<
/Annots [195 0 R 196 0 R 197 0 R 198 0 R 199 0 R 200 0 R 201 0 R]
/Contents [202 0 R 203 0 R 204 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 205 0 R
/Font 206 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi12 207 0 R
>>
>>
/Type /Page
>>
endobj
22 0 obj
<<
/Annots [208 0 R 209 0 R 210 0 R 211 0 R 212 0 R 213 0 R]
/Contents [214 0 R 215 0 R 216 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 217 0 R
/Font 218 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi13 219 0 R
>>
>>
/Type /Page
>>
endobj
23 0 obj
<<
/Annots [220 0 R 221 0 R 222 0 R 223 0 R 224 0 R 225 0 R 226 0 R 227 0 R 228 0 R]
/Contents [229 0 R 230 0 R 231 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 232 0 R
/Font 233 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi14 234 0 R
>>
>>
/Type /Page
>>
endobj
24 0 obj
<<
/Annots [235 0 R]
/Contents [236 0 R 237 0 R 238 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 239 0 R
/Font 240 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi15 241 0 R
>>
>>
/Type /Page
>>
endobj
25 0 obj
<<
/Annots [242 0 R 243 0 R 244 0 R 245 0 R 246 0 R 247 0 R 248 0 R 249 0 R]
/Contents [250 0 R 251 0 R 252 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 253 0 R
/Font 254 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi16 255 0 R
>>
>>
/Type /Page
>>
endobj
26 0 obj
<<
/Annots [256 0 R 257 0 R 258 0 R 259 0 R 260 0 R 261 0 R 262 0 R]
/Contents [263 0 R 264 0 R 265 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 266 0 R
/Font 267 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi17 268 0 R
>>
>>
/Type /Page
>>
endobj
27 0 obj
<<
/Annots [269 0 R 270 0 R 271 0 R 272 0 R]
/Contents [273 0 R 274 0 R 275 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 276 0 R
/Font 277 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi18 278 0 R
>>
>>
/Type /Page
>>
endobj
28 0 obj
<<
/Annots [279 0 R 280 0 R 281 0 R 282 0 R 283 0 R 284 0 R 285 0 R 286 0 R 287 0 R]
/Contents [288 0 R 289 0 R 290 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 291 0 R
/Font 292 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi19 293 0 R
>>
>>
/Type /Page
>>
endobj
29 0 obj
<<
/Annots [294 0 R 295 0 R]
/Contents [296 0 R 297 0 R 298 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 299 0 R
/Font 300 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi20 301 0 R
>>
>>
/Type /Page
>>
endobj
30 0 obj
<<
/Annots [302 0 R 303 0 R 304 0 R 305 0 R 306 0 R 307 0 R 308 0 R]
/Contents [309 0 R 310 0 R 311 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 312 0 R
/Font 313 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi21 314 0 R
>>
>>
/Type /Page
>>
endobj
31 0 obj
<<
/Annots [315 0 R 316 0 R 317 0 R 318 0 R 319 0 R 320 0 R]
/Contents [321 0 R 322 0 R 323 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 324 0 R
/Font 325 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi22 326 0 R
>>
>>
/Type /Page
>>
endobj
32 0 obj
<<
/Annots [327 0 R 328 0 R 329 0 R 330 0 R 331 0 R 332 0 R 333 0 R]
/Contents [334 0 R 335 0 R 336 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 337 0 R
/Font 338 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi23 339 0 R
>>
>>
/Type /Page
>>
endobj
33 0 obj
<<
/Annots [340 0 R 341 0 R 342 0 R 343 0 R 344 0 R 345 0 R 346 0 R 347 0 R]
/Contents [348 0 R 349 0 R 350 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 351 0 R
/Font 352 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi24 353 0 R
>>
>>
/Type /Page
>>
endobj
34 0 obj
<<
/Annots [354 0 R]
/Contents [355 0 R 356 0 R 357 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 358 0 R
/Font 359 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi25 360 0 R
>>
>>
/Type /Page
>>
endobj
35 0 obj
<<
/Annots [361 0 R 362 0 R 363 0 R 364 0 R 365 0 R 366 0 R 367 0 R 368 0 R 369 0 R]
/Contents [370 0 R 371 0 R 372 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 373 0 R
/Font 374 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi26 375 0 R
>>
>>
/Type /Page
>>
endobj
36 0 obj
<<
/Annots [376 0 R 377 0 R 378 0 R 379 0 R 380 0 R 381 0 R 382 0 R 383 0 R 384 0 R 385 0 R
386 0 R 387 0 R 388 0 R 389 0 R 390 0 R 391 0 R 392 0 R 393 0 R 394 0 R 395 0 R
396 0 R 397 0 R 398 0 R 399 0 R 400 0 R 401 0 R 402 0 R 403 0 R 404 0 R 405 0 R
406 0 R]
/Contents [407 0 R 408 0 R 409 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 410 0 R
/Font 411 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi27 412 0 R
>>
>>
/Type /Page
>>
endobj
37 0 obj
<<
/Annots [413 0 R 414 0 R 415 0 R 416 0 R 417 0 R 418 0 R 419 0 R 420 0 R 421 0 R 422 0 R
423 0 R 424 0 R 425 0 R 426 0 R 427 0 R]
/Contents [428 0 R 429 0 R 430 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 431 0 R
/Font 432 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi28 433 0 R
>>
>>
/Type /Page
>>
endobj
38 0 obj
<<
/Annots [434 0 R 435 0 R 436 0 R 437 0 R 438 0 R 439 0 R 440 0 R 441 0 R 442 0 R 443 0 R
444 0 R 445 0 R]
/Contents [446 0 R 447 0 R 448 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 449 0 R
/Font 450 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi29 451 0 R
>>
>>
/Type /Page
>>
endobj
39 0 obj
<<
/Annots [452 0 R 453 0 R 454 0 R 455 0 R 456 0 R 457 0 R 458 0 R 459 0 R 460 0 R 461 0 R
462 0 R 463 0 R 464 0 R 465 0 R 466 0 R 467 0 R 468 0 R 469 0 R 470 0 R 471 0 R
472 0 R 473 0 R 474 0 R 475 0 R 476 0 R 477 0 R 478 0 R 479 0 R 480 0 R 481 0 R]
/Contents [482 0 R 483 0 R 484 0 R]
/MediaBox [0 0 486 720]
/Parent 4 0 R
/Resources <<
/ExtGState 485 0 R
/Font 486 0 R
/ProcSet [/PDF /Text /ImageB /ImageC /ImageI]
/XObject <<
/Xi30 487 0 R
>>
>>
/Type /Page
>>
endobj
40 0 obj
<<
/Count 2
/Dest [9 0 R /Fit]
/First 488 0 R
/Last 489 0 R
/Next 490 0 R
/Parent 3 0 R
/Prev 6 0 R
/Title (1 Introduction)
>>
endobj
41 0 obj
<<
/Dest [38 0 R /Fit]
/Next 7 0 R
/Parent 3 0 R
/Prev 491 0 R
/Title (Acknowledgments)
>>
endobj
42 0 obj
<<
/Length 1358
/Filter /FlateDecode
>>
stream
xXIoF7 +6E
Ҹ)lHh/X,H-
'͐پ}o~h=i>viZCM2cn~˥~n8(/ǜb`wLME3S6m̿[EccGq.&b!D"+17يoCwaCDX)nXcC|lf!t6o[Wkx3WJSgGpـ7Đ-gn"ĜAZOCAߦVKښs(oC%+q,;-9IGhSY=$Xez/l8ԨsMuoŠN+jA舋+"h+1'+D|-/ę8xY!&$|"Ba֤+_Sr"7q[YFNwoY!c`
Um7UJ*A6o` 3RLA{%
Ԛ)!+k
SC'"{xސh<].qpPfV'j>S,UMCʎD_ԟGfTrB`sd̥c;=/HLTXѮsV8-vJ`W&T%r
>ogx.,y4'*
~͍O&z Iaxa^P17\y*--Lr@ԛ0Y٫@pHƘh̉uB\gC;'nC^g!]\yFT&soָ
J#vjgCG?>Qul/WͲf{#U9jizbѷeDv52&;%K%KF:'!ZLcT/yzO]jŤf)o38їX%" CʛQ i8F-+FġsƏ13[J»|7^e%:U!L2; vD
FR
vp EāʾABR&6Z<WEBm
in-tH'<,8O &c! LCREq5JF"~v-`ŠQ/Q
j4o#QBWXi0$PLBC]e}|K.u
z3O4ECӸC9NvqfV_:/[ŃAϩtXu?'$a9NyXfC]gYqhՑMJSJUcv^1J/-uS/^/~'
endstream
endobj
43 0 obj
<<
/Subtype /Type0
/Type /Font
/BaseFont /DRAVLV+ArialUnicodeMS
/Encoding /Identity-H
/DescendantFonts [492 0 R]
/ToUnicode 493 0 R
>>
endobj
44 0 obj
<<
/Length 1732
/Subtype /Form
/Filter /FlateDecode
/Type /XObject
/Matrix [1 0 0 1 0 0]
/FormType 1
/Resources <<
/ColorSpace <<
/Cs1 [/ICCBased 494 0 R]
>>
/ProcSet [/PDF /Text]
/ExtGState <<
/Gs1 495 0 R
/Gs2 496 0 R
>>
/Font <<
/TT2 497 0 R
>>
>>
/BBox [0 0 595 842]
>>
stream
xˎ^5)6om uxQd_+e6T[5|
_C.F=|KG=,u)nz5|xzsx~wiVb=?=qz8zȣINC}@>ȟfLmgR(ߊtkM9ڣu=^/l)GK I