Rencontre, 20 septembre 2018
La rencontre aura lieu en Amphi B (3ème étage, site Monod)
Programme
 10:30 – 12:00

Thomas Streicher (Univ. Darmstadt (DE))Invited talk: How Unique are Ground Models
Guided by basic topos theory we discuss the notion of "ground model" and how unique it is. We describe a few negative results and finish with discussing why the question is open for classical realizability.
 14:00 – 15:00

Guillaume Geoffroy (Institut de Mathématiques de Marseille)Invited talk: Connecting degrees of parallelism and Boolean algebras through classical realizability
Nonfully abstract models of PCF and related systems typically contain socalled nonsequential functions : for example, Scott's model of continuous functions has parallel or, while Berry's stable functions have Gustave's function. Using constructs which come from Krivine's classical relizability (notably the characteristic Boolean algebra Gimel 2), we show how these nonsequential functions and the question of their relative strength (in terms of their ability to emulate oneanother) can be connected to the theory of Boolean algebras.
 15:30 – 16:30

Henning Basold (CNRS  ENS de Lyon)
Coinduction is a powerful definition, programming and reasoning method that can be applied in a variety of situations, such as automata theory, reactive systems, modal logic, potentially infinite data, nonterminating computations etc. Typically, coinduction is understood as the fact that bisimilarity implies equality in the denotational semantics. However, coinduction can be extended to other predicates and relations on statebased systems, thereby providing for general coinductive programming and reasoning techniques.
I will present in this talk foundations for recursive proof search in coinductive Horn clause specifications, aka coinductive logic programs. Such specifications have a wide range of applications: coinductive programming, type class resolution, type checking and more. Because of applications like type class resolution, we will focus on constructive methods for proof search. In particular, we will discuss a firstorder intuitionistic sequent calculus with recursion for coinductive predicates, a system of coinductive uniform proofs that will enable proof search, and we will study the relation of these proof system to each other and to complete Herbrand models.