Invited Tutorial Speakers

Automatic Structures: Twenty Years Later

THU, 09.07.2020, 14:00-15:00 UTC+2 | When is this in my timezone?

Automatic structures made their appearance at LICS twenty years ago, at LICS 2000. However, their roots are much older. The idea of automata based decision procedures for logical theories can be traced back to the early days of automata theory and to the work of Büchi, Elgot, Trakhtenbrot and Rabin in the 1960s. The explicit notion of automatic structures has first been proposed in 1976 in the (unfortunately largely unnoticed) PhD thesis of Hodgson, and later been reinvented by Khoussainov and Nerode in 1995.

In this tutorial, we present an introduction into the history and basic definitions of automatic structures, and survey the achievements in the study of different variants of automatic structures. We discuss their most important mathematical and algorithmic properties, their characterisations in terms of logical interpretations, and we present some of the mathematical techniques that are used for the analysis of automatic structures and for proving limitations of these concepts. Read more …

Contextual Types, Explained: Invited Tutorial

FRI, 10.07.2020, 17:00-18:00 UTC+2 | When is this in my timezone?

Contextual objects characterize an object M together with the typing context Ψ in which it is meaningful. This idea is then also internalized within the type theory itself using the notion of a contextual type which pairs the type A of an object together with the context Ψ in which the object is well-typed. In this tutorial, we review the origins of this idea and show its power in characterizing partial programs, mechanizing meta-theory, and meta-programming. Starting from the simply typed setting, we give an overview of existing work which adopts contextual types to dependent type theories and touch on future research directions. Read more …