Richard Zach

I will provide a (very basic) tutorial on the Curry-Howard correspondence between proofs (in natural deduction) and terms in the typed -calculus. No prior knowledge of either will be presupposed.

I will provide a (very basic) tutorial on the Curry-Howard correspondence between proofs (in natural deduction) and terms in the typed λ-calculus. No prior knowledge of either will be presupposed.

Many scientific questions are considered solved to the best possible degree when we have a method for computing a solution. This is especially true in mathematics and those areas of science in which phenomena can be described mathematically: one only...