curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

Diffstat

1 file changed, 144 insertions, 0 deletions

diff --git a/images/agda.eps b/images/agda.eps
@@ -0,0 +1,144 @@
+%!PS-Adobe-3.0 EPSF-3.0
+%%Creator: cairo 1.17.6 (https://cairographics.org)
+%%CreationDate: Sun Oct  9 19:42:20 2022
+%%Pages: 1
+%%DocumentData: Clean7Bit
+%%LanguageLevel: 2
+%%Title: logotype
+%%BoundingBox: 0 0 3612 980
+%%EndComments
+%%BeginProlog
+50 dict begin
+/q { gsave } bind def
+/Q { grestore } bind def
+/cm { 6 array astore concat } bind def
+/w { setlinewidth } bind def
+/J { setlinecap } bind def
+/j { setlinejoin } bind def
+/M { setmiterlimit } bind def
+/d { setdash } bind def
+/m { moveto } bind def
+/l { lineto } bind def
+/c { curveto } bind def
+/h { closepath } bind def
+/re { exch dup neg 3 1 roll 5 3 roll moveto 0 rlineto
+      0 exch rlineto 0 rlineto closepath } bind def
+/S { stroke } bind def
+/f { fill } bind def
+/f* { eofill } bind def
+/n { newpath } bind def
+/W { clip } bind def
+/W* { eoclip } bind def
+/BT { } bind def
+/ET { } bind def
+/BDC { mark 3 1 roll /BDC pdfmark } bind def
+/EMC { mark /EMC pdfmark } bind def
+/cairo_store_point { /cairo_point_y exch def /cairo_point_x exch def } def
+/Tj { show currentpoint cairo_store_point } bind def
+/TJ {
+  {
+    dup
+    type /stringtype eq
+    { show } { -0.001 mul 0 cairo_font_matrix dtransform rmoveto } ifelse
+  } forall
+  currentpoint cairo_store_point
+} bind def
+/cairo_selectfont { cairo_font_matrix aload pop pop pop 0 0 6 array astore
+    cairo_font exch selectfont cairo_point_x cairo_point_y moveto } bind def
+/Tf { pop /cairo_font exch def /cairo_font_matrix where
+      { pop cairo_selectfont } if } bind def
+/Td { matrix translate cairo_font_matrix matrix concatmatrix dup
+      /cairo_font_matrix exch def dup 4 get exch 5 get cairo_store_point
+      /cairo_font where { pop cairo_selectfont } if } bind def
+/Tm { 2 copy 8 2 roll 6 array astore /cairo_font_matrix exch def
+      cairo_store_point /cairo_font where { pop cairo_selectfont } if } bind def
+/g { setgray } bind def
+/rg { setrgbcolor } bind def
+/d1 { setcachedevice } bind def
+/cairo_data_source {
+  CairoDataIndex CairoData length lt
+    { CairoData CairoDataIndex get /CairoDataIndex CairoDataIndex 1 add def }
+    { () } ifelse
+} def
+/cairo_flush_ascii85_file { cairo_ascii85_file status { cairo_ascii85_file flushfile } if } def
+/cairo_image { image cairo_flush_ascii85_file } def
+/cairo_imagemask { imagemask cairo_flush_ascii85_file } def
+%%EndProlog
+%%BeginSetup
+%%EndSetup
+%%Page: 1 1
+%%BeginPageSetup
+%%PageBoundingBox: 0 0 3612 980
+%%EndPageSetup
+q 0 0 3612 980 rectclip
+1 0 0 -1 0 980 cm q
+0 g
+213.75 216 m 213.75 227.184 204.684 236.25 193.5 236.25 c 182.312 236.25
+ 173.25 227.184 173.25 216 c 173.25 204.816 182.312 195.75 193.5 195.75 
+c 204.684 195.75 213.75 204.816 213.75 216 c h
+213.75 216 m f*
+288.75 216 m 288.75 227.184 279.684 236.25 268.5 236.25 c 257.312 236.25
+ 248.25 227.184 248.25 216 c 248.25 204.816 257.312 195.75 268.5 195.75 
+c 279.684 195.75 288.75 204.816 288.75 216 c h
+288.75 216 m f*
+27 w
+1 J
+1 j
+[] 0.0 d
+4 M q 1 0 0 1 0 0 cm
+763.5 13.5 m 463.5 313.5 l S Q
+q 1 0 0 1 0 0 cm
+913.5 88.5 m 763.5 238.5 l S Q
+q 1 0 0 1 0 0 cm
+913.5 13.5 m 763.5 163.5 l S Q
+q 1 0 0 1 0 0 cm
+388.5 13.5 m 238.5 163.5 l S Q
+q 1 0 0 1 0 0 cm
+463.5 13.5 m 313.5 163.5 l S Q
+q 1 0 0 1 0 0 cm
+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
+ 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
+ 913.5 163.5 l S Q
+q 1 0 0 1 0 0 cm
+913.5 763.5 m 1665 13.5 l 1665 763.5 l S Q
+0 J
+0 j
+q 1 0 0 1 0 0 cm
+1183.5 493.875 m 1663.875 493.875 l S Q
+q 1 0 0 1 0 0 cm
+2308.5 493.5 m 2308.5 642.617 2187.613 763.5 2038.5 763.5 c 1889.383 763.5
+ 1768.5 642.617 1768.5 493.5 c 1768.5 344.383 1889.383 223.5 2038.5 223.5
+ c 2187.613 223.5 2308.5 344.383 2308.5 493.5 c h
+2308.5 493.5 m S Q
+1 J
+1 j
+q 1 0 0 1 0 0 cm
+2308.5 223.5 m 2308.5 696 l 2308.5 846 2188.5 966 2038.5 966 c 1937.805
+ 966 1850.633 911.926 1804.199 831 c S Q
+0 J
+0 j
+q 1 0 0 1 0 0 cm
+2953.5 493.5 m 2953.5 642.617 2832.613 763.5 2683.5 763.5 c 2534.383 763.5
+ 2413.5 642.617 2413.5 493.5 c 2413.5 344.383 2534.383 223.5 2683.5 223.5
+ c 2832.613 223.5 2953.5 344.383 2953.5 493.5 c h
+2953.5 493.5 m S Q
+1 J
+1 j
+q 1 0 0 1 0 0 cm
+2953.875 13.5 m 2953.875 763.5 l S Q
+0 J
+0 j
+q 1 0 0 1 0 0 cm
+3598.5 493.5 m 3598.5 642.617 3477.613 763.5 3328.5 763.5 c 3179.383 763.5
+ 3058.5 642.617 3058.5 493.5 c 3058.5 344.383 3179.383 223.5 3328.5 223.5
+ c 3477.613 223.5 3598.5 344.383 3598.5 493.5 c h
+3598.5 493.5 m S Q
+1 J
+1 j
+q 1 0 0 1 0 0 cm
+3598.5 223.5 m 3598.5 763.5 l S Q
+Q Q
+showpage
+%%Trailer
+end
+%%EOF