Live-Coding Mathematics Your First Clojure Proof - Frederic Peschanski

Have you heard about the lambda-calculus, dependent types, intuitionistic v.s. classical logic, or the Curry-Howard correspondence?

During this talk you will learn much about these, but not presented in the usual academic way... No! Clojure and Emacs/Cider will serve as learning vehicles, throughout a gently-paced live-coding Mathematics session !

For this we will use LaTTe, an open source proof assistant library for Clojure, probably one of the most addictive single-player puzzle game ever!

NB: no greek letters were harmed during the preparation of this talk.