LoCal: Logic and Computation

Head of team : Thomas Seiller

Seminars and other events related to the team’s activities can be found on the shared calendar.

Research topics

The LoCal team (Logic and Computation) was created on January 1st 2025, following the split of the previous LoVe team (Logic and Verification) along its two independent research axes (Logic on one hand, Verification on the other). Research in the LoCal team concerns logic and/or computational complexity.

More precisely, our research covers:

• the theory of programming languages and the proofs-as-programs correspondence,
• semantics: of programming languages, of linear logic, of type theory,
• category theory, and in particular topos theory and higher categories,
• the formalization of mathematics, and in particular numerical and functional analysis,
• several approaches to computational complexity with, or without, relations with logic (implicit complexity, descriptive complexity, algebraic complexity, Kolmogorov complexity).