style:

Connexion:

This page

Programme

  • La rencontre commence le lundi à 14h et se termine le vendredi vers midi.
  • En fait pour l'instant, à cause d'un faux contact dans l'amphi, on est en salle 65, 4 cantons.
  • Les exposés ont lieu dans l'amphithéâtre du bâtiment 4 cantons (en rouge sur le plan).
  • Les exposés contribués durent environ 30 minutes questions comprises.
  • On ne remplira sans doute pas tous les créneaux, afin de laisser de la place aux discussions entre les participants... et aux pauses au bord du lac.

Lundi 8 juin

Mardi 9 juin

Mercredi 10 juin

Jeudi 11 juin

Vendredi 12 juin

Résumés

Valentin Blot

Typed realizability for first-order classical analysis

Résumé: We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed lambda-mu calculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to intuitionistic logic. We prove that the usual terms of Gödel's system T realize the axioms of Peano arithmetic, and that under some assumptions on the computational model, the bar recursion operator realizes the axiom of dependent choice. We also perform a proper analysis of relativization, which allows for less technical proofs of adequacy. Extraction of algorithms from proofs of Pi-0-2 formulas relies on a clever implementation of Friedman's trick exploiting the control possibilities of the language. This allows to have extracted programs with simpler types than in the standard case.

Florent Bréhard

Un calcul des séquents pour les treillis distributifs avec action *-continus

Résumé: Les treillis distributifs avec action *-continus sont des algèbres de Kleene étendues avec des opérateurs d'intersection et de résiduation, dont les deux modèles principaux sont les relations binaires sur un ensemble et les langages rationnels sur alphabet. Un ensemble de travaux récents s'attache à concevoir des calculs de séquents pour ces treillis (entre autres), sans pour l'instant parvenir à incorporer la distributivité de l'intersection sur l'union sans casser l'élimination des coupures. Nous proposons une solution à ce problème.

Dominique Duval

Relative Hilbert-Post completeness for exceptions

Résumé: I will introduce a relative notion of syntactic completeness and sketch a proof of the fact that adding exceptions to a programming language can be done in such a way that the completeness of the underlying language is preserved. This proof has been checked with the proof assistant Coq. This work has been done in collaboration with Jean-Guillaume Dumas, Burak Ekici, Damien Pous and Jean-Claude Reynaud.

Clovis Eberhart

Presheaves for Processes and Unfoldings

We propose a general framework for graph rewriting systems based on presheaves, close in spirit to Baldan et al.'s work using adhesive categories. We emphasise the construction of processes and unfoldings of Petri nets.

Arnaud Germain

Préordres, solos et typage

Marie Kerjean

Reduction strategies in differential lambda-calculus

Résumé: Ehrhard and Regnier's differential lambda-calculus is an extension of the lambda-calculus with a notion of linear application. This linear application is defined together with the notion of linear substitution; one considers sums of terms to deal with some non-determinism coming from the choice of which occurence is substituted. We consider linear substitution as an active reduction, and give a variant of differential lambda-calculus without sums. It then appears that the definition of linear substitution considered by Ehrhard and Regnier is inherently call-by-name. This definition can be translated into an adaptation of the Krivine abstract Machine, or into an embedding in the Pi-calculus. We give then a call-by-value version of linear substitution, which can also be adapted into an abstract machine or a Pi-calculus embedding. We dicusss whether the idea of a deterministic differential lambda-calculus can be adapted to proof-terms.

Rodolphe Lepigre

A Realizability Model for a Semantical Value Restriction

Résumé: Reconciling dependent product and classical logic with call-by-value evaluation is a difficult problem. It is the first step toward a classical proof system for an ML-like language. In such a system, the introduction rule for universal quantification and the elimination rule for dependent product need to be restricted: they can only be applied to values. This value restriction is acceptable for universal quantification (ML-like polymorphism) but makes dependent product unusable in practice.

In order to circumvent this limitation we introduce new typing rules and prove their consistency by constructing a realizability model in three layers (values, stacks and terms). Such a technique has already been used to account for classical ML-like polymorphism in call-by-value, and here we extend it to handle dependent products. The main idea is to internalize observational equivalence as a new non-computable operation. A crucial property of the model is that the biorthogonal of a set of values which is closed under observational equivalence does not contain more values than the original set.

Guillaume Munch

Intuitionistic Depolarisation with Polarised Realizability

Résumé: Polarisation is the presence of an evaluation order characterised by lack of associativity of composition. The depolarisation of intuitionistic logic corresponds to the fact that the order of evaluation does not matter, thanks to referential transparency and strong normalisation. This depolarisation is for instance an ingredient of parametricity (I will sketch why). I recently proposed a polarised, Curry-style, approach to the extensional lambda calculus with pairs and sums. (Recall that Curry-style lambda calculus with sums does not exist because co-products are inconsistent in the presence of arbitrary fixed points.) This approach suggests that associativity of composition should not be seen as a syntactic axiom but as an emergent property akin to normalisation. Traditionally, the issue has rather been considered to be with extensionality. In this talk I will more formally relate intuitionistic depolarisation to strong normalisation. I fit the development in a general setting of polarised realizability structures (inspired by Girard, Krivine) for classical and intuitionistic logics, and observational models built from them (inspired by Pitts and Stark). I stress that the intuitionistic character does not come from a restriction to intuitionistic realizability, but from the referentially-transparent nature of computation stemming from the absence of control operators.

Thomas Seiller

Graphings

Résumé: Graphings are a generalization of graphs which were primarily used in ergodic theory and functional analysis. Based on geometry of interaction techniques, one can define interpretations of linear logic proofs as graphings and build quantitative realizability models for linear logic or strict fragments of it, such as elementary linear logic. The construction of such models is quite general and provides a rich hierarchy that reflects subtle distinctions in terms of computational complexity, while adapting to several computational paradigms. For instance, one can find infinite families of models capturing distinct sub-logarithmic classes, in their deterministic, non-deterministic and probabilistic variants.