URegina Topology and Geometry Seminar: Joseph Eremondi

In this talk, I'll introduce the Simply Typed Lambda Calculus (STLC), describing how it connects constructive propositional logic and computation. I then discuss how Cartesian Closed Categories serve as models of the STLC, and how the categorical perspective can be used to prove foundational results about the STLC, such as:

• There are no proofs of falsehood in the base STLC
• Law of the Excluded Middle is not derivable in STLC without additional axioms.
• All closed boolean programs evaluate to "true" or "false" (canonicity)
• The correspondence between datatypes and initial algebras.