Propositions as Types Simple Energy Curry–Howard isomorphism Types and Programming Languages @parametricity Type safe printf Brian's talk at Strangeloop 2014