Philip Wadler provides an in depth discussion on the Curry–Howard correspondence [0] in his paper Propositions as Types [1], and he has given several talks unde

Philip Wadler provides an in depth discussion on the Curry–Howard correspondence [0] in his paper Propositions as Types [1], and he has given several talks under the same name that are on YouTube. The talk Prof Wadler gave at Strange Loop is the most cited, but the talk he gave at Stanford [2] is the most interesting because Carl Hewitt was in the audience and was challenging him on the merits and long-term viability of functional programming in general vs Hewitt's Actor Model [3] for scalable concurrent computing. [0] Curry–Howard correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence [1] Propositions as Types [pdf] http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-... [2] Propositions as Types (Stanford) [video] https://www.youtube.com/watch?v=ivzpaiw26wQ https://www.youtube.com/watch?v=ivzpaiw26wQ Slides [pdf] http://www.inf.ed.ac.uk/teaching/courses/tspl/pat.pdf http://www.inf.ed.ac.uk/teaching/courses/tspl/pat.pdf [3] Actor Model https://en.wikipedia.org/wiki/Category:Actor_model_(computer_science) https://en.wikipedia.org/wiki/Category:Actor_model_(computer...