The Curry-Howard Isomorphism for Propositional Logic

Published: Jan. 2, 2020, 9 p.m.

Discussion of the Curry-Howard isomorphism for the connectives of propositional logic (AND, OR, NOT, FALSE, IMPLIES).\xa0 Initial consideration of Curry-Howard for first-order and higher-order logic.\xa0 Dependent types.