Bartosz Milewski

Blogger at BartoszMilewski.com. Moslty about programming and category theory.

Bartosz started as a quantum physicist, joined Microsoft to build the search engine for Windows and became an avid proponent of OOP. Then he got into concurrency and parallelism and now he’s evangelizing FP. He is an author of a book Category Theory for Programmers.

Keynote: The Truth about Types

Lots of programmers, especially our brethren who use JavaScript, Python, or Closure, don't appreciate the power of strong static typing. Haskell programmers, on the other hand, eat types for breakfast, lunch, and dinner. Types are not just hints for the compiler to better catch programming errors. They encode logic. I'll talk about the Curry-Howard-Lambek isomorphism between types and logic. We can encode, in types, truth and falsehood; conjunction, disjunction, and implication; and let the Haskell compiler prove logical theorems for us.

Slides
Video ←Back