The speaker for this week’s seminar is Rafaël Bocquet from the Laboratoire des Sciences du Numérique de Nantes. Please find the title and abstract below. Rafaël will give the talk remotely on zoom.

Title

Relative induction principles for the syntax of type theory

Abstract

The syntax and semantics of dependent type theories and other languages with variable binders can be presented in either a first-order or a higher-order way. Both perspectives are useful. The first-order presentation has well-behaved semantics, but the first-order encoding of the notions of variables, substitutions, etc. can be hard to work with. The higher-order presentations are easier to work with, but do not immediately come with an induction principle. I will present relative induction principles, which provide a way to perform induction over syntax without the bureaucracy of the first-order encoding.This is based on my recently defended PhD thesis “Relative induction principles for second-order generalized algebraic theories” (https://rafaelbocquet.gitlab.io/pdfs/thesis.pdf).