Posted on November 16, 2018 by Marko Dimjašević Benjamin C. Pierce writes what it is like to use a proof assistant to teach programming language foundations. Tags: Curry-Howard, logic, programming languages, proof assistant, teaching, type theory, ephemera, functional programming