Topology and Geometry Seminar

Location: AH 347

Speaker: Joseph Eremondi, University of Regina

Title: The noncommutative geometry of cubes and prisms

Abstract:  

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.

This event is sponsored by PIMS.