%PDF-1.5
%
1 0 obj
<<
/Metadata 2 0 R
/Names 3 0 R
/OpenAction 4 0 R
/Outlines 5 0 R
/PageMode /UseOutlines
/Pages 6 0 R
/Type /Catalog
>>
endobj
7 0 obj
<<
/Author ()
/CreationDate (D:20200624165440+02'00')
/Creator (LaTeX with hyperref)
/Keywords ()
/ModDate (D:20211026124747+02'00')
/PTEX.Fullbanner (This is pdfTeX, Version 3.14159265-2.6-1.40.21 \(TeX Live 2020/Debian\) kpathsea version 6.3.2)
/Producer (pdfTeX-1.40.21)
/Subject ()
/Title ()
/Trapped /False
>>
endobj
2 0 obj
<<
/Length 3818
/Subtype /XML
/Type /Metadata
>>
stream
application/pdf
2020-06-24T16:54:40+02:00
LaTeX with hyperref
2021-10-26T12:47:47+02:00
2021-10-26T12:47:47+02:00
pdfTeX-1.40.21
False
This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020/Debian) kpathsea version 6.3.2
uuid:819546a6-47ac-4ced-830c-36a2839800b7
uuid:818463cc-73d7-444a-8df2-f51eb57353ba
endstream
endobj
3 0 obj
<<
/Dests 8 0 R
>>
endobj
4 0 obj
<<
/D [9 0 R /FitV]
/S /GoTo
>>
endobj
5 0 obj
<<
/Count 39
/First 10 0 R
/Last 11 0 R
/Type /Outlines
>>
endobj
6 0 obj
<<
/Count 19
/Kids [12 0 R 13 0 R 14 0 R]
/Type /Pages
>>
endobj
8 0 obj
<<
/Kids [15 0 R 16 0 R]
/Limits [(AMS.4) (subsection.Appendix.A.3)]
>>
endobj
9 0 obj
<<
/Annots [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]
/Contents [35 0 R 36 0 R 37 0 R 38 0 R 39 0 R 40 0 R 41 0 R 42 0 R]
/CropBox [0 0 612 792]
/MediaBox [0 0 612 792]
/Parent 12 0 R
/Resources 43 0 R
/Rotate 0
/Type /Page
>>
endobj
10 0 obj
<<
/A 44 0 R
/Next 45 0 R
/Parent 5 0 R
/Title (I Introduction)
>>
endobj
11 0 obj
<<
/A 46 0 R
/Parent 5 0 R
/Prev 47 0 R
/Title (Appendix C: Soundness)
>>
endobj
12 0 obj
<<
/Count 7
/Kids [48 0 R 9 0 R 49 0 R 50 0 R 51 0 R 52 0 R 53 0 R]
/Parent 6 0 R
/Type /Pages
>>
endobj
13 0 obj
<<
/Count 6
/Kids [54 0 R 55 0 R 56 0 R 57 0 R 58 0 R 59 0 R]
/Parent 6 0 R
/Type /Pages
>>
endobj
14 0 obj
<<
/Count 6
/Kids [60 0 R 61 0 R 62 0 R 63 0 R 64 0 R 65 0 R]
/Parent 6 0 R
/Type /Pages
>>
endobj
15 0 obj
<<
/Kids [66 0 R 67 0 R 68 0 R 69 0 R 70 0 R 71 0 R]
/Limits [(AMS.4) (section.10)]
>>
endobj
16 0 obj
<<
/Kids [72 0 R]
/Limits [(section.2) (subsection.Appendix.A.3)]
>>
endobj
17 0 obj
<<
/A <<
/D (cite.flowcaml)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [155.727 156.032 162.8 166.976]
/Subtype /Link
/Type /Annot
>>
endobj
18 0 obj
<<
/A <<
/D (cite.ZdancewicThesis)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [172.657 156.032 179.73 166.976]
/Subtype /Link
/Type /Annot
>>
endobj
19 0 obj
<<
/A <<
/D (cite.assumptionsguarantees)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [267.754 156.032 274.827 166.976]
/Subtype /Link
/Type /Annot
>>
endobj
20 0 obj
<<
/A <<
/D (cite.SecCSL)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [284.683 156.032 296.838 166.976]
/Subtype /Link
/Type /Annot
>>
endobj
21 0 obj
<<
/A <<
/D (cite.OHEARN2007)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [119.13 96.256 131.085 107.2]
/Subtype /Link
/Type /Annot
>>
endobj
22 0 obj
<<
/A <<
/D (cite.brookes:csl)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [141.705 96.256 153.66 107.2]
/Subtype /Link
/Type /Annot
>>
endobj
23 0 obj
<<
/A <<
/D (cite.flowcaml)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [238.792 72.402 245.666 83.346]
/Subtype /Link
/Type /Annot
>>
endobj
24 0 obj
<<
/A <<
/D (cite.assumptionsguarantees)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [255.761 72.402 262.635 83.346]
/Subtype /Link
/Type /Annot
>>
endobj
25 0 obj
<<
/A <<
/D (cite.CovernMain)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [272.729 72.402 279.603 83.346]
/Subtype /Link
/Type /Annot
>>
endobj
26 0 obj
<<
/A <<
/D (cite.comp-ni-sep)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [289.698 72.402 296.572 83.346]
/Subtype /Link
/Type /Annot
>>
endobj
27 0 obj
<<
/A <<
/D (cite.SecCSL)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [314.365 598.43 326.52 609.373]
/Subtype /Link
/Type /Annot
>>
endobj
28 0 obj
<<
/A <<
/D (cite.CovernValueDep)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [477.107 526.798 484.08 537.667]
/Subtype /Link
/Type /Annot
>>
endobj
29 0 obj
<<
/A <<
/D (cite.DynSecLabels)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [494.701 526.798 506.656 537.667]
/Subtype /Link
/Type /Annot
>>
endobj
30 0 obj
<<
/A <<
/D (cite.GregersenIdris)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [516.28 526.798 528.235 537.667]
/Subtype /Link
/Type /Annot
>>
endobj
31 0 obj
<<
/A <<
/D (cite.comp-ni-sep)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [516.257 312.772 523.132 323.715]
/Subtype /Link
/Type /Annot
>>
endobj
32 0 obj
<<
/A <<
/D (cite.SecCSL)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [532.641 312.772 544.397 323.715]
/Subtype /Link
/Type /Annot
>>
endobj
33 0 obj
<<
/A <<
/D (cite.iris1)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [439.029 72.402 450.785 83.346]
/Subtype /Link
/Type /Annot
>>
endobj
34 0 obj
<<
/A <<
/D (cite.irisJFP)
/S /GoTo
>>
/Border [0 0 0]
/C [0 1 0]
/H /O
/Rect [460.176 72.402 471.932 83.346]
/Subtype /Link
/Type /Annot
>>
endobj
35 0 obj
<<
/Length 862
/Filter /FlateDecode
>>
stream
H|U˒6+xˏr $m(+94=
fnjf^g2Vg\"2Vu%Ӳl!v^[#ǼJ>[S7^-(ӫCV^v
ޔm]6xH_"'ei@(vJ
~#M^Ij^R4PxY55);&
QtxV5Uvcw;$V&^&FK
1n8nƎz/i^$Mxǜw_]V4C.OvTβP*mVTMY w/.6 38otYZVp8q;'90CNq[Ρq+Zh$p`
;El 6 ]&nJ>S,Ԥpd
>F2ip1Js\QxCT?i{hEo)
s9cd?c,O ݨBR dy59\HuW }(,y@B QOFE1
aM\}j#tCw'OJi