EVENT

Event News

JFLI seminar by Dr. Thomas Seiller & Dr. Marie Kerjean, CNRS LIPN

We are pleased to inform you about the upcoming seminar by Dr. Thomas Seiller & Dr. Marie Kerjean, CNRS LIPN, Everyone interested is cordially invited to attend!

Title:

Logical structures arising from corpora

Speaker:

Dr. Thomas Seiller, CNRS LIPN

Abstract:

The impressive results obtained by generative language models witness that statistical information about a (large enough) corpus can be used to extract some structure of natural langage. As part of a general effort to investigate how to mathematically understand this process, Bradley, Gastaldi and Terilla have proposed a generalisation of the standard notion of formal concepts to incorporate quantitative information. This approach consists in moving from sets to functions over sets (using presheaves): the generalised formal concepts are thus obtained as so-called nuclei (fixed points) of an adjunction. In this talk I will explain how this generalisation of formal concepts turns out to coincide with linear realisability, a technique to define models of (fragments of) linear logic. This leads to a dual structure on nuclei defined from textual corpora: a geometric structure, represented by a tropical cell complex, and a logical structure.

Bio:

Thomas Seiller is a research scientist at CNRS, a member of the LIPN laboratory, and an associated researcher at the Institut d'Histoire et de Philosophie des Sciences et des Techniques (IHPST). He obtained his PhD in 2012, supervised by Jean-Yves Girard and Laurent Regnier. Prior to joining CNRS, he held several postdoctoral fellowships, including a Carmin fellowship at the Institut des Hautes Études Scientifiques (IHÉS) and a Marie Curie fellowship at the University of Copenhagen. From 2021 to 2025, he served as scientific secretary of the CNRS theoretical computer science evaluation committee and as a member of the board of the interdisciplinary evaluation committee "Science in Society".His research focuses on logic and the mathematical foundations of computer science, including linear logic and realizability techniques, semantics (operational and denotational), computational complexity (in particular: complexity and logic, algebraic complexity, and Kolmogorov complexity), static analysis and automatic program transformation, dynamical systems and randomness, as well as the philosophical aspects of computer science.

Title:

From functional programming to functional analysis and back

Speaker:

Dr. Marie Kerjean, CNRS LIPN

Abstract:

In this presentation, we will review some of the motivations and challenges associated with interpreting proofs as functions in continuous contexts, as well as the computational characteristics that can be extracted from traditional functional analysis. Thanks to the Curry-Howard correspondence, programmes are typed by proofs, which can in turn be interpreted as functions between spaces. By following this path in the opposite direction, one can extract functions from new paradigms in logic. The historical example is linearity, which has evolved from an algebraic notion to a computational one. Partly driven by applications in probabilistic and differential programming, we try to make notions from analysis follow the same path. We will explain how to integrate differentiation into the framework of proof theory. We will show how this new perspective on differentiation allows us to connect some of Gödel's work to algorithmic differentiation. If time permits, we will show how functional analysis and distribution theory provides us with a monadic framework for the quantitative interpretation of proofs and programmes.

Bio:

Marie Kerjean is a CNRS researcher in Logic, affiliated to the LIPN (Université Sorbonne Paris Nord). She obtained her PhD in 2018 from Université Paris Diderot. She is the recipient of the 2019 Young talent award from L'Oreal - Académie des Sciences, and of distinguished paper awards from FSCD 2023 and LICS 2025. She specializes in the denotational semantics of proofs and programs, as well as in the formalization of analysis in the Rocq proof assistant.