curry-howard

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

Mode Name Size
-rw-r--r-- .gitignore 17L
-rw-r--r-- LICENSE 1L
-rw-r--r-- README.md 4L
-rw-r--r-- examples/eq.lean 4L
-rw-r--r-- examples/example.lean 7L
-rw-r--r-- examples/exhaustion-naive.py 3L
-rw-r--r-- examples/exhaustion.py 2L
-rw-r--r-- examples/factorial.py 5L
-rw-r--r-- examples/fake-theorem.py 1L
-rw-r--r-- examples/gen-hacker.py 14L
-rw-r--r-- examples/hacker.txt 5L
-rw-r--r-- examples/liquid.lean 6L
-rw-r--r-- examples/nat.lean 3L
-rw-r--r-- examples/sqrt.py 1L
-rw-r--r-- examples/typechecking.c 9L
-rw-r--r-- examples/types.lean 7L
-rw-r--r-- examples/types.py 5L
-rw-r--r-- images/agda.eps 144L
-rw-r--r-- images/coq.png 6269B
-rw-r--r-- images/kepler.eps 580L
-rw-r--r-- images/lean.eps 172L
-rw-r--r-- images/pentium.png 775023B
-rw-r--r-- images/watchmen.eps 113L
-rw-r--r-- main.tex 466L
-rw-r--r-- preamble.tex 71L