just to note this talk briefly alludes to another subject, the Curry–Howard isomorphism, something Philip Wadler had similarly given a talk about at Lambda Days

just to note this talk briefly alludes to another subject, the Curry–Howard isomorphism, something Philip Wadler had similarly given a talk about at Lambda Days (2016) titled 'Propositions as Types'[1] (slides [2] and the video recording[3]). [1]: http://www.lambdadays.org/lambdadays2016/philip-wadler http://www.lambdadays.org/lambdadays2016/philip-wadler [2]: http://www.lambdadays.org/static/upload/media/1456226071518855propositionsastypeskrakow.pdf http://www.lambdadays.org/static/upload/media/14562260715188... [3]: https://youtu.be/aeRVdYN6fE8 https://youtu.be/aeRVdYN6fE8