If you are interested in giving a talk (in person or over Zoom), then please contact Alvaro (apintado $$ sas $$ upenn $$ edu).
Upcoming Talks
-
Categorical Semantics for Simply-typed Lambda Calculi
Speaker: Oualid Merzouga
Date: November 24, 2025
Abstract: This talk presents a semantic tour of the simply typed λ-calculus equipped with function types, products, and coproducts. When all three are present, the categorical interpretation is natural: cartesian closed categories provide a clear and intuitive setting where products model conjunction, coproducts capture disjunction, and exponentials represent implication.
Things become subtler when only function types remain. In the absence of products and coproducts, the familiar cartesian structure disappears, and with it the usual intuition for interpreting exponentials. The central goal of the talk is to motivate and develop the more delicate categorical framework required to model this fragment, highlighting what structural resources are lost and what must replace them. This talk marks the start of a short series where we will investigate an extension of simple typed lambda calculus to substructural and modal logics--The following week--as well as a talk moving the needle further into classical systems territory--next semester--.
The presentation assumes basic familiarity with category theory and aims to give an accessible picture of the semantic landscape that emerges once the comfort of cartesian structure is removed.
Past Talks