Topic 3: Propositions as types: type theory vs set theory
Section outline
-
In the next topic, we will extend our focus to type theory. Originally developed by Russell and Whitehead in response to set-theoretic paradoxes, it started to be influential due to connections with functional programming and constructive mathematics. Let us start by reading a paper by Wadler, "Propositions as types" and Zach "The significance of Curry-Howard isomorphism" to gain some initial understanding of the concepts.