Corelab Seminar

Alex Kavvos
On the Semantics of Intensionality and Intensional Recursion

Intensionality is a phenomenon that occurs in logic and computation. In the most general sense, a function is intensional if it operates at a level finer than (extensional) equality. This is a familiar setting for computer scientists, who often study different programs or processes that are interchangeable, i.e. extensionally equal, even though they are not implemented in the same way, so intensionally distinct. Concomitant with intensionality is the phenomenon of intensional recursion, which refers to the ability of a program to have access to its own code. This talk is concerned with crafting a logical toolkit through which these phenomena can be studied. Our main contribution is a framework in which mathematical and computational constructions can be considered either extensionally, i.e. as abstract values, or intensionally, i.e. as fine-grained descriptions of their construction. The main tool in this is modal type theory, where we use a modality to express intensionality in a programming language. We then use category theory to provide a semantics for the aforementioned language, through the novel notion of exposure. The device of exposures is also useful in studying the interplay between extension and intension, as well as in proving abstract analogues of classic results with an intensional flavour, e.g. Goedel's First Incompleteness Theorem, Tarski's Undefinability Theorem, Rice's Theorem, and Kleene's Second Recursion Theorem.