Joseph Eremondi

Building on last week's talk, I discuss Locally Cartesian Closed Categories (LCCCs) , in which every slice category is Cartesian Closed. I describe how these categories serve model quantifiers in logic, as well as modelling type dependencies in a way...

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...