Logic Seminar - Thorsten Altenkirch
| Dates: | 22 October 2025 |
|---|
| Times: | 15:00 - 16:00 |
|---|
| What is it: | Seminar |
|---|
| Organiser: | Department of Mathematics |
|---|
| Who is it for: | University staff, External researchers, Current University students |
|---|
|
Speaker: Thorsten Altenkirch (University of Nottingham)
How to Define Type Theories?
Traditionally, type theories have been defined extrinsically—by sorting untyped terms. In this talk, I will present the intrinsic approach, where we never introduce untyped objects. This can be implemented using Quotient Inductive–Inductive Types (QIITs), allowing us to establish fundamental results such as normalisation within the same framework. In this setting, the so-called initiality theorem becomes immediate: the syntax of type theory is by definition an initial algebra. This leads to some interesting questions. The usual syntax is set-based, but how can we even define the standard model interpreting types as sets? I will sketch how to address this coherence problem. Another topic is how to eliminate much of the boilerplate in traditional presentations. Ambrus Kaposi has proposed the use of SOGATs (second-order algebraic theories), which can be seen as a principled revival of higher-order abstract syntax. These ideas also yield very concise definitions of well-known systems, such as first-order predicate logic. This talk is based on joint work with several collaborators, most notably Ambrus Kaposi.
Travel and Contact Information
Find event
Frank Adams 1
Alan Turing Building
Manchester
