Invited speakers

In constructive mathematics, an ongoing challenge is to extracting computational content from infinitary arguments in classical mathematics — especially those that yield concrete results via abstract tools such as minimal bad sequences or maximal ideals. Today, a wide range of such techniques exists, constituting a late partial fulfillment of Hilbert's program.

This talk presents work in progress on porting the modal operators "everywhere" and "somewhere", as developed in set theory by Joel David Hamkins, Victoria Gitman and their collaborators, into type theory. This modal enrichment provides a uniform language for expressing several established constructivization techniques, and is at the core of a relatively recent new technique that offers insights on the origins of some of our most cherished inductive definitions. These developments are closely connected to recent advances in type-theoretic presheaf and sheaf models, dialogue continuity, synthetic algebraic geometry and well-quasi-order theory.

Intuitionistic modal logic, despite more than seventy years of investigation, still partly escapes our comprehension. Structural proof theoretic accounts of intuitionistic modal logic have adopted either the paradigm of labelled deduction in the form of labelled natural deduction and sequent systems, or the one of unlabelled deduction in the form of sequent or nested sequent systems. Both approaches are still under active consideration. In this talk, I would like to give an overview of the current landscape of intuitionistic modal proof theory and survey some of the more recent developments.

PDF version of abstract with references.

Focusing and polarity are two intertwined ideas that relate proofs and computation, informing modern ideas about canonical forms, pattern matching, evaluation order, logical frameworks, and logic programming in the proof-search-as-computation paradigm. However, the relationship between these ideas, their history, and the underlying proof theory, remain obscure and folkloric to many practitioners. This talk will serve as beginner’s guide for the uninitiated, attempting to reconcile disparate presentations, separate orthogonal concepts, signpost the landscape of important prior work in the area, and gesture at promising paths for further investigation.

In homotopy type theory, every type effectively carries the structure of a higher groupoid: a set equipped with a higher-dimensional equivalence relation. Conversely, there ought to be an effective interpretation of homotopy type theory in higher groupoids. Unfortunately, Voevodsky's model in Kan simplicial sets is non-constructive. And existing cubical models fail to constructively present higher groupoids in the above sense.

In this talk, I will introduce an effective interpretation of homotopy type theory in higher groupoids. This is based on a combination of cubical and semisimplicial techniques.