Program

Schedule

Detailled schedule in the making... Please check again later.

	Morning	Afternoon
Tuesday		Invited lecture: Alexandre Miquel
Wednesday	Invited course: Martin Hofmann	Invited lecture: Jean-Louis Krivine
Thursday	Invited course: Martin Hofmann	Federico Aschieri, Mauricio Guillermo, Hugo Herbelin
Friday	Invited lecture: Jonas Frey	Christophe Raffalli, Giovanni Birolo, Cyrus Nourani

Invited Speakers

1. Martin Hofmann: Proof-relevant logical relations
   Logical predicates and logical relations have been used in a variety of situations ranging from realizability, program extraction to justification of data abstraction and rigorous proof of program equivalences.
   If logical predicates are used in connection with dynamic allocation then typically the defining clause ("realisation relation" in the terminology of realisability) for computation types involves existential quantification over "future worlds", i.e. possible extensions of the store. Such existential quantifiers generate a host of technical difficulties and various partial solutions have been proposed including the use of continuations and double negation closures. None of them has so far been entirely satisfactory.
   We present here a novel approach which works by replacing the existential quantification with a proof relevant Sigma type. Accordingly, since logical relations represent a kind of abstract equality, the resulting proof-relevant logical relations represent a proof-relevant equality which is known from the groupoid interpretation of type theory.
   The talks will review logical relations with existential quantification and some of the known work, recall the groupoid model of type theory and then describe our current state of knowledge about proof-relevant logical relations and how they allow us to establish program equivalences that are not reachable with current methods.
   This is joint & ongoing work with Vivek Nigam, Andrew Kennedy, Nick Benton

2. Jean-Louis Krivine: Some properties of classical realizability models (slides)
   Classical realizability models of ZF which are proper (i.e. not given by forcing) have a much more complicated structure than forcing models, and they are only superficially understood up to now. We shall give some general properties and look at some particular models. We will show that true arithmetical formulas, and even \Pi_1^1 formulas are realized; that a model is proper iff its characteristic Boolean algebra is non trivial. We will build proper models in which the characteristic Boolean algebra is finite. T. Ehrhard and also T. Streicher have shown that the usual models of lambda-calculus have, in fact, a structure of realizability algebra. Therefore, they give rise to realzability models. We will study a simple case, which is a proper realizability model, in which integers are preserved.

3. Jonas Frey: Basic relational objects as an algebraic framework for realizability (slides)
   Indexed/fibred preorders are a good framework to organize and analyze realizability interpretations, in particular when interested in their model theoretic aspects. We introduce the approach to realizability via fibred preorders and illustrate the preceding claim by giving some examples.
   We then introduce "basic relational objects", which are representations of fibred preorders inspired by Hofstra's "basic combinatory objects" and Longley's "computability structures". The category of basic relational objects has good closure properties and is general enough to encompass many known realizability constructions such as Kleene realizability, Kreisel's modified realizability (in a certain sense), Goedel's dialectica interpretation, and Krivine's classical realizability. Furthermore, the category of basic relational objects contains all preorders and all triposes.
   Viewing BROs as generalized preorders, we introduce generalizations of the constructions of presheaves and sheaves to BROs, which allows to view the effective topos as a generalized presheaf topos. This point of view allows to give an abstract characterization of realizability toposes on partial combinatory algebras, and demonstrates in particular how the concept of partial combinatory algebra arises naturally from a few abstract assumptions.

4. Alexandre Miquel: Constructing classical realizability models of set theory. (slides)
   The aim of this talk is to present Krivine's construction of classical realizability models of Zermelo-Fraenkel set theory (ZF). For that, I will first introduce the theory ZF-epsilon, a non-extensional version (and a conservative extension) of ZF that distinguishes two membership relations: a non extensional membership predicate, which is primitive, and the usual extensional membership predicate, which is defined from the former by extensional collapse. From this, I will construct a model of Pi-names (parameterized by an arbitrary realizability algebra), and show that all the axioms of ZF-epsilon are realized in this model. In particular, I will discuss the important problem of the existence/non-existence of witnesses in the model (depending on whether the considered existential property is extensional or not), and I will show how this construction relates with Boolean valued models and Tarski models of ZF.

Contributed talks

1. Federico Aschieri: Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms. (slides)
   Interactive realizability is a computational semantics of classical Arithmetic. It is based on interactive learning and was originally designed to interpret excluded middle and Skolem axioms for simple existential formulas. A realizer represents a proof/construction depending on some state, which is an approximation of some Skolem functions. The realizer interacts with the environment, which may provide a counter-proof, a counterexample invalidating the current construction of the realizer. But the realizer is always able to turn such a negative outcome into a positive information, which consists in some new piece of knowledge learned about the mentioned Skolem functions. In this talk, we extend Interactive realizability to a system which includes classical first-order Peano Arithmetic with Skolem axioms. For witness extraction, the learning capabilities of realizers will be exploited according to the paradigm of learning by levels. In particular, realizers of atomic formulas will be update procedures in the sense of Avigad and thus will be understood as stratified-learning algorithms.

2. Mauricio Guillermo: Krivine's Realizers from Kreisel's no-counterexample interpretations.
   This talk is about an application of the Specification of arithmetical Formulae. We present breafly the specification problem, which consists in the characterization of the universal realizers of a given formula in terms of its computational behaviour [1]. First, we deal with the case where the language of realizers does not contain instructions incompatible with substitutive constants (in the sense of [1]). For this particular case, we generalize the result proven in [2] for an arbitrary number of alternations of quantifiers. This generalization is part of the work of E. Miquey during his internship at Montevideo, see [3]. Second, we present the general case, whithout any assumptions about the instructions allowed in the language of classical realizers. We show that in this case, we have realizers that not satisfies the specification given before. This case, as in [1], must be trated with a more sophisticated game and the proof of the specification leans strongly on the Threads Method introduced in [2] and improved in [1]. Third, we explain how to build realizers of arithmetical formulae by programming the recursive functionals given by the no-counterexample interpretation. Our goal is to satisfy the specification in order to build the realizer.
   • [1]"Specifying Peirce's Law in Classical Realizability". M. Guillermo & A. Miquel. To appear in MSCS.
   • [2]"Realizability games in arithmetical formulae". M Guillermo. PhD Thesis 2008.
   • [3] "Realizing Arithmetical Formulae". E. Miquey. Internship 2011.

3. Hugo Herbelin: A Computational Proof of Dependent Choice Compatible with Classical Logic. (slides)
   Choice is derivable from strong existential quantification (Sigma-types) in Martin-Löf's intuitionistic type theory. Strong existential elimination is not compatible in general with a computational approach of classical logic but it can still be accomodated with computational classical logic if one enforces a call-by-value normalisation semantics of proofs and restrict strong existential elimination to proofs that are locally intuitionistic.
   If, in addition, we interpret countable universal quantification as an infinite conjunction that we evaluate, not in call-by-value (because it would take an infinite time) but in call-by-need, then, the proof of countable choice from intuitionistic type theory can be reformulated in this logic with strong existential and classical reasoning, leading to a computational proof of countable choice (namely \forall n \exists x P(n,x) -> \exists f \forall n P(n,f(n))) compatible with classical reasoning. This scales to dependent choice and bar induction.
   A comparison with Krivine's quote-based "proof" of countable choice will be sketched.

4. Christophe Raffalli: Extracting program from the "infinite tape lemma.
   "The infinite tape lemma" is the (trivial) result saying that an infinite stream of 0s and 1s contains infinitely many 0s or infinitely many 1s. Remark that this lemma is the only classical lemma needed to prove Ramsey theorem ! As an illustration of realisability, from this classical lemma, we will extract a program that gives a sequence of n ones or n zeros from an infinite boolean sequence. We will also see that the program is not symmetric, it gives sequences of bits that are consecutive in the original sequence for either the 0 or the 1. Can this be fixed ? Can we obtain a sequence using always the first bits in the original sequence ?

5. Giovanni Birolo: Classical program extraction by examples
   We present some examples of applications of a realization interpretation for classical logic we call interactive realizability. We consider classical proofs of simple geometrical and combinatorial facts requiring excluded middle over semi-decidable statements. These facts may be expressed by simple existential statements and their computational contents are actual programs that produce a geometric or combinatorial object with the required properties. We conclude with some remarks on the readability and computational complexity of these programs.

6. Cyrus Nourani: (cancelled) Functorial Models, Horn Products, and Positive Omitting Types Realizability.
   Link to abstract
   Link to slides

Restaurant on Wednesday evening

For those interested, we will have diner at the restaurant "Les Halles" in the center of Chambéry. The address is 15 rue Bonivard 73000 Chambery. The easiest is to go there by bus from the campus: bus number 9, stop "Éléphants". (timetable)

Here is a small (Google)map for reaching the restaurant from the bus stop: map.

We will meet there at 7'15 pm, and the reservation is for "colloque réalisabilité".

To come back on the campus, you'll have to take the only night bus leaving from "Éléphants" at 11'00 pm.

Apéritif / barbecue on Thursday

The weather permiting, we will have a barbecue at the "Plage des Mottets". You can take bus 1 to go there (one bus every half-hour until 8.pm), or walk there (36 minutes acording to Google map): map.