Michael Bernstein on Propositions as Types

It's going to be a special evening. After taking the month of July off, we're coming back with the original (https://www.meetup.com/papers-we-love/events/163406212/) Papers We Love speaker, Michael R. Bernstein (http://michaelrbernste.in), co-host of Beats, Rye, & Types (http://beatsryetypes.com/) and Code Climate (https://codeclimate.com/) hustler, and he’s very excited to be back, presenting on Propositions as Types (http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf) by Philip Wadler (http://homepages.inf.ed.ac.uk/wadler/) and showcasing some work from The Little Prover (http://the-little-prover.github.io/) by Friedman (http://www.cs.indiana.edu/~dfried/) and Eastlund (http://www.ccs.neu.edu/home/cce/)!

Intro

I’ll (Michael) be talking about Philip Wadler’s paper "Propositions as Types," which starts out with the following sentence:

"Powerful insights arise from linking two fields of study previously thought separate."

And just keeps on going from there. In less than 9 full pages, Wadler assembles an exuberant, hilarious take on the deep, meaningful connections between mathematics, philosophy, and computer science.

I’ll also be showing off some work from Daniel P. Friedman and Carl Eastlund’s recent book "The Little Prover (https://mitpress.mit.edu/books/little-prover)," which implements a small theorem prover in Scheme, to demonstrate some of the connections Wadler discusses in his paper.

Bio

Michael R. Bernstein (http://michaelrbernste.in) (@mrb_bk (http://twitter.com/mrb_bk)) loves you. He lives in Takoma Park, MD and spends most of his time thinking about pottery, obscure LPs, food, and the intersection of philosophy and Computer Science.