Pellucid

Letting Curry-Howard Code for Me

Written by Alexandre Bertails on October 15, 2014

Pellucid Analytics' Data and Scala expert gives a talk at NY Scala on the Curry-Howard Isomorphism. Below is the video and abstract.

"Letting Curry-Howard Code for Me"

Alexander Bertails - "Let Curry-Howard code for me" at NY Scala Content

Did you know that types are propositions and that programs are their proofs? You may have heard that before but have you ever wondered what it means?

In this short talk, I will simply go through the proof of a very simple theorem, and show the intuitions behind the Curry-Howard isomorphism that will let us extract a program from our proof!