Hi guys, I'm talking about the deep and fascinating correspondence between logic and computation in this talk. This is a very "there is no spoon" no kind of topic, which is the kind of thing I think is quite fun to explore. On a practically level it's also pretty much a prerequisite for understanding the principles that modern type inference is built on.
The talk is primarily based around this tutorial on the Curry-Howard correspondence and natural deduction:
See you there!