Paul Snively on Propositions as Types

Los Angeles - February 24, 2016

Paul Snively on Propositions as Types


Philip Wadler may be the most important computer scientist you’ve never heard of. However, as principal designer of the Haskell programming language, co-designer of generics in Java with Scala designer Martin Odersky, co-designer of XQuery for the W3C, and prolific (and humorous, cf. ’Threesomes, with and without blame’ from POPL 2010) writer and speaker, there is little doubt he has influenced you if you write software. His recent (March 2014) paper, 'Propositions as Types,' is his survey of the relationship between propositions, as in mathematical logic, and types, as in statically-typed programming language. Together, we’ll explore how and why this relationship is broad, deep, and mysterious; how it may shape new and future programming languages and possibly affect STEM education; and maybe even shed a little light (and hopefully a little less heat) on why some users of statically-typed languages are so adamant about it.


Paul Snively is an architect for Verizon OnCue, working in Scala in a purely functional fashion. He loves both building things other people use and thinking about how and why the things he builds work, and like many other people, has discovered that the best way to learn is to try to teach, so he led a workshop on formal logic at the Scala World conference in 2015, which he later re-recorded as a screencast; he discussed Type Systems: The Good, The Bad, and The Ugly at the Strange Loop conference in 2014 with Amanda Laucher; and he discussed Types vs. Tests: An Epic Battle? at the Strange Loop conference in 2012, also with Amanda Laucher.

Yahoo Papers We Love Los Angeles would like to thank Yahoo for hosting this month's meetup.