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 |
