curry-howard
Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
agda.eps (4454B)
1 %!PS-Adobe-3.0 EPSF-3.0 2 %%Creator: cairo 1.17.6 (https://cairographics.org) 3 %%CreationDate: Sun Oct 9 19:42:20 2022 4 %%Pages: 1 5 %%DocumentData: Clean7Bit 6 %%LanguageLevel: 2 7 %%Title: logotype 8 %%BoundingBox: 0 0 3612 980 9 %%EndComments 10 %%BeginProlog 11 50 dict begin 12 /q { gsave } bind def 13 /Q { grestore } bind def 14 /cm { 6 array astore concat } bind def 15 /w { setlinewidth } bind def 16 /J { setlinecap } bind def 17 /j { setlinejoin } bind def 18 /M { setmiterlimit } bind def 19 /d { setdash } bind def 20 /m { moveto } bind def 21 /l { lineto } bind def 22 /c { curveto } bind def 23 /h { closepath } bind def 24 /re { exch dup neg 3 1 roll 5 3 roll moveto 0 rlineto 25 0 exch rlineto 0 rlineto closepath } bind def 26 /S { stroke } bind def 27 /f { fill } bind def 28 /f* { eofill } bind def 29 /n { newpath } bind def 30 /W { clip } bind def 31 /W* { eoclip } bind def 32 /BT { } bind def 33 /ET { } bind def 34 /BDC { mark 3 1 roll /BDC pdfmark } bind def 35 /EMC { mark /EMC pdfmark } bind def 36 /cairo_store_point { /cairo_point_y exch def /cairo_point_x exch def } def 37 /Tj { show currentpoint cairo_store_point } bind def 38 /TJ { 39 { 40 dup 41 type /stringtype eq 42 { show } { -0.001 mul 0 cairo_font_matrix dtransform rmoveto } ifelse 43 } forall 44 currentpoint cairo_store_point 45 } bind def 46 /cairo_selectfont { cairo_font_matrix aload pop pop pop 0 0 6 array astore 47 cairo_font exch selectfont cairo_point_x cairo_point_y moveto } bind def 48 /Tf { pop /cairo_font exch def /cairo_font_matrix where 49 { pop cairo_selectfont } if } bind def 50 /Td { matrix translate cairo_font_matrix matrix concatmatrix dup 51 /cairo_font_matrix exch def dup 4 get exch 5 get cairo_store_point 52 /cairo_font where { pop cairo_selectfont } if } bind def 53 /Tm { 2 copy 8 2 roll 6 array astore /cairo_font_matrix exch def 54 cairo_store_point /cairo_font where { pop cairo_selectfont } if } bind def 55 /g { setgray } bind def 56 /rg { setrgbcolor } bind def 57 /d1 { setcachedevice } bind def 58 /cairo_data_source { 59 CairoDataIndex CairoData length lt 60 { CairoData CairoDataIndex get /CairoDataIndex CairoDataIndex 1 add def } 61 { () } ifelse 62 } def 63 /cairo_flush_ascii85_file { cairo_ascii85_file status { cairo_ascii85_file flushfile } if } def 64 /cairo_image { image cairo_flush_ascii85_file } def 65 /cairo_imagemask { imagemask cairo_flush_ascii85_file } def 66 %%EndProlog 67 %%BeginSetup 68 %%EndSetup 69 %%Page: 1 1 70 %%BeginPageSetup 71 %%PageBoundingBox: 0 0 3612 980 72 %%EndPageSetup 73 q 0 0 3612 980 rectclip 74 1 0 0 -1 0 980 cm q 75 0 g 76 213.75 216 m 213.75 227.184 204.684 236.25 193.5 236.25 c 182.312 236.25 77 173.25 227.184 173.25 216 c 173.25 204.816 182.312 195.75 193.5 195.75 78 c 204.684 195.75 213.75 204.816 213.75 216 c h 79 213.75 216 m f* 80 288.75 216 m 288.75 227.184 279.684 236.25 268.5 236.25 c 257.312 236.25 81 248.25 227.184 248.25 216 c 248.25 204.816 257.312 195.75 268.5 195.75 82 c 279.684 195.75 288.75 204.816 288.75 216 c h 83 288.75 216 m f* 84 27 w 85 1 J 86 1 j 87 [] 0.0 d 88 4 M q 1 0 0 1 0 0 cm 89 763.5 13.5 m 463.5 313.5 l S Q 90 q 1 0 0 1 0 0 cm 91 913.5 88.5 m 763.5 238.5 l S Q 92 q 1 0 0 1 0 0 cm 93 913.5 13.5 m 763.5 163.5 l S Q 94 q 1 0 0 1 0 0 cm 95 388.5 13.5 m 238.5 163.5 l S Q 96 q 1 0 0 1 0 0 cm 97 463.5 13.5 m 313.5 163.5 l S Q 98 q 1 0 0 1 0 0 cm 99 313.5 13.5 m 13.5 313.5 l 163.5 313.5 l 163.5 463.5 l 163.5 628.5 298.5 100 763.5 463.5 763.5 c 628.5 763.5 763.5 628.5 763.5 463.5 c 763.5 313.5 l 101 913.5 163.5 l S Q 102 q 1 0 0 1 0 0 cm 103 913.5 763.5 m 1665 13.5 l 1665 763.5 l S Q 104 0 J 105 0 j 106 q 1 0 0 1 0 0 cm 107 1183.5 493.875 m 1663.875 493.875 l S Q 108 q 1 0 0 1 0 0 cm 109 2308.5 493.5 m 2308.5 642.617 2187.613 763.5 2038.5 763.5 c 1889.383 763.5 110 1768.5 642.617 1768.5 493.5 c 1768.5 344.383 1889.383 223.5 2038.5 223.5 111 c 2187.613 223.5 2308.5 344.383 2308.5 493.5 c h 112 2308.5 493.5 m S Q 113 1 J 114 1 j 115 q 1 0 0 1 0 0 cm 116 2308.5 223.5 m 2308.5 696 l 2308.5 846 2188.5 966 2038.5 966 c 1937.805 117 966 1850.633 911.926 1804.199 831 c S Q 118 0 J 119 0 j 120 q 1 0 0 1 0 0 cm 121 2953.5 493.5 m 2953.5 642.617 2832.613 763.5 2683.5 763.5 c 2534.383 763.5 122 2413.5 642.617 2413.5 493.5 c 2413.5 344.383 2534.383 223.5 2683.5 223.5 123 c 2832.613 223.5 2953.5 344.383 2953.5 493.5 c h 124 2953.5 493.5 m S Q 125 1 J 126 1 j 127 q 1 0 0 1 0 0 cm 128 2953.875 13.5 m 2953.875 763.5 l S Q 129 0 J 130 0 j 131 q 1 0 0 1 0 0 cm 132 3598.5 493.5 m 3598.5 642.617 3477.613 763.5 3328.5 763.5 c 3179.383 763.5 133 3058.5 642.617 3058.5 493.5 c 3058.5 344.383 3179.383 223.5 3328.5 223.5 134 c 3477.613 223.5 3598.5 344.383 3598.5 493.5 c h 135 3598.5 493.5 m S Q 136 1 J 137 1 j 138 q 1 0 0 1 0 0 cm 139 3598.5 223.5 m 3598.5 763.5 l S Q 140 Q Q 141 showpage 142 %%Trailer 143 end 144 %%EOF