Rencontre, 20 septembre 2018

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

Non-fully abstract models of PCF and related systems typically contain so-called non-sequential 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 non-sequential functions and the question of their relative strength (in terms of their ability to emulate one-another) can be connected to the theory of Boolean algebras.

15:30 – 16:30

Henning Basold (CNRS - ENS de Lyon)

Invited talk: Foundations for Corecursive Proof Search with Horn Clauses

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, non-terminating 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 state-based 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 first-order 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.