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

[1] 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 Slides [pdf] http://www.inf.ed.ac.uk/teaching/courses/tspl/pat.pdf

[3] Actor Model https://en.wikipedia.org/wiki/Category:Actor_model_(computer...