Curry-Howard correspondence (Moriconi)

This topic refers to the course About the Curry-Howard correspondence (Moriconi). Here is a description and a bibliography for addressing it.

• E. Moriconi, "Steps towards a proof-theoretic semantics", in Topoi, 31 (1), 2012

• W. A. Howard, "The formulae-as-types notion of construction", in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, 1980, pp. 479-491

• P. Wadler, "Proposition as types", in Communications of the ACM, 58 (12), December 2015, pp. 75-84

• R. Zach, "The significance of the Curry-Howard Isomorphism", in Philosophy of logic and mathematics, 2019, pp. 313-326