Liste d'articles pour l'évaluation du cours Outils classiques pour la correspondance preuves-programmes

• il s'agira d'une sorte de fiche de synthèse critique;
• il sera à remettre une semaine avant votre soutenance;
• ce document pourra faire jusqu'à 4 pages en LaTeX ou 8 pages manuscrites;
• il devra répondre aux éléments détaillés plus haut (problématique scientifique, contexte, résultats exposés, outils et idées techniques) notamment par la rédaction d'un résumé/synthèse de l'article et par l'explication du cadre et les développements techniques de l'article. Vous pourrez si cela vous semble pertinent exposer une preuve de l'article ou au moins ses grandes lignes.
• la fiche de synthèse servira de base à la présentation orale

• les présentation auront lieu au cours du semestre, à partir du 11 mars, les dates et horaires seront précisés ultérieurement;
• la présentation durera une vingtaine de minutes et sera suivie de questions;
• vous disposerez du tableau et pourrez projeter des transparents (il n'y a aucune obligation à préparer des slides). Dans tous les cas, nous souhaiterions qu'une partie de votre exposé se fasse au tableau;
• la présentation devra s'adresse aux enseignants mais également à vos camarades

Propositional Gödel logic G extends intuitionistic logic with the non-constructive principle of linearity (A→B)∨(B→A). We introduce a Curry–Howard correspondence for G and show that a simple natural deduction calculus can be used as a typing system. The resulting functional language extends the simply typed λ-calculus via a synchronous communication mechanism between parallel processes, which increases its expressive power. The normalization proof employs original termination arguments and proof transformations implementing forms of code mobility. Our results provide a computational interpretation of G, thus proving A. Avron’s 1991 thesis.

We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms (and not only on proof-nets): subject reduction is satisfied and a well-typed term admits a polynomial bound on the length of any of its beta reduction sequences. We also give a translation of LAL into DLAL and deduce from it that all polynomial time functions can be represented in DLAL.

Functional Reactive Programming (FRP) models reactive systems with events and signals, which have previously been observed to correspond to the “eventually” and “always” modalities of linear temporal logic (LTL). In this paper, we define a constructive vari- ant of LTL with least fixed point and greatest fixed point opera- tors in the spirit of the modal mu-calculus, and give it a proofs-as- programs interpretation as a foundational calculus for reactive pro- grams. Previous work emphasized the propositions-as-types part of the correspondence between LTL and FRP; here we emphasize the proofs-as-programs part by employing structural proof theory. We show that the type system is expressive enough to enforce liveness properties such as the fairness of schedulers and the eventual de- livery of results. We illustrate programming in this calculus using (co)iteration operators. We prove type preservation of our opera- tional semantics, which guarantees that our programs are causal. We give also a proof of strong normalization which provides justi- fication that our programs are productive and that they satisfy live- ness properties derived from their types.

We show how solutions to many recursive arena equations can be computed in a natural way by allowing loops in arenas. We then equip arenas with winning functions and total winning strategies. We present two natural winning conditions compatible with the loop con- struction which respectively provide initial algebras and terminal coal- gebras for a large class of continuous functors. Finally, we introduce an intuitionistic sequent calculus, extended with syntactic constructions for least and greatest fixed points, and prove it has a sound and (in a certain weak sense) complete interpretation in our game model.

We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a fully fledged quantum programming language in which entanglement, duplication, and recursion are all available. This model is an instance of a new framework which captures not only quantum but also classical and probabilistic computation. Its main feature is the ability to model commutative effects in a parallel setting. Our model comes with a multi-token machine, a proof net system, and a PCF-style language. Being based on a multi-token machine equipped with a memory, it has a concrete nature which makes it well suited for building low-level operational descriptions of higher-order languages.

Modal μ -calculus is one of the central logics for verification. In his seminal paper, Kozen proposed an axiomati- zation for this logic, which was proved to be complete, 13 years later, by Kaivola for the linear-time case and by Walukiewicz for the branching-time one. These proofs are based on complex, non-constructive arguments, yielding no reasonable algorithm to construct proofs for valid formulas. The problematic of constructiveness becomes central when we consider proofs as certificates, supporting the answers of verification tools. In our paper, we provide a new completeness argument for the linear- time μ -calculus which is constructive, i.e. it builds a proof for every valid formula. To achieve this, we decompose this difficult problem into several easier ones, taking advantage of the correspondence between the μ -calculus and automata theory. More precisely, we lift the well-known automata transformations (non-determinization for instance) to the logical level. To solve each of these smaller problems, we perform first a proof-search in a circular proof system, then we transform the obtained circular proofs into proofs of Kozen’s axiomatization.

We present and study a simple Call-By-Push-Value lambda- calculus with fix-points and recursive types. We explain its connection with Linear Logic by presenting a denotational interpretation of the lan- guage in any model of Linear Logic equipped with a notion of embedding retraction pairs. We consider the particular case of the Scott model of Linear Logic from which we derive an intersection type system for our calculus and prove an adequacy theorem. Last, we introduce a fully po- larized version of this calculus which turns out to be a term language for a large fragment of LLP and refines lambda-mu.

We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.

Nakano’s later modality allows types to express that the output of a function does not immediately depend on its input, and th us that computing its fixpoint is safe. This idea, guarded recur sion, has proved useful in various contexts, from functional prog ramming with infinite data structures to formulations of step-i ndexing internal to type theory. Categorical models have revealed t hat the later modality corresponds in essence to a simple reindexin g of the discrete time scale. Unfortunately, existing guarded type theories suffer from s ignificant limitations for programming purposes. These limit ations stem from the fact that the later modality is not expressive e nough to capture precise input-output dependencies of functions . As a consequence, guarded type theories reject many productive definitions. Combining insights from guarded type theories and synchro- nous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behave d reindexing of the time scale to a type. We call such reindexings time warps . Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ou rs.

We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on ‘quasi-Borel predomains’. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore’s axiomatic domain theory and a model of Kock’s synthetic measure theory.

We describe here a simple method in order to obtain programs from proofs in second-order classical logic. Then we extend to classical logic the results about storage operators (typed λ-terms which simulate call-by-value in call-by-name) proved by Krivine (1990) for intuitionistic logic. This work generalizes previous results of Parigot (1992).

The category Rel of sets and relations yields one of the simplest denotational semantics of Linear Logic (LL). It is known that Rel is the biproduct completion of the Boolean ring. We consider the generalization of this construction to an arbitrary continuous semiring R, producing a cpo-enriched category which is a semantics of LL, and its (co)Kleisli category is an adequate model of an extension of PCF, parametrized by R. Specific instances of R allow us to compare programs not only with respect to “what they can do”, but also “in how many steps” or “in how many different ways” (for non-deterministic PCF) or even “with what probability” (for probabilistic PCF).

We revisit many aspects of the syntactic relations between (variants of ) classical linear logic (LL) and (variants of ) intuitionistic linear logic (ILL) in the propositional setting. On the one hand, we study different (parametric) “negative” translations from LL to ILL: their expressiveness, the relations with extensions of LL and their use in the proof theory of LL (cut elimination and focusing). In particular, this bridges the intuitionistic restriction on sequents (at most one conclusion) and the focusing property of linear logic. On the other hand, we generalise the known partial results about conservativity of LL over ILL, leading for example to a conservativity proof for LL over tensor logic (TL).

Starting from an exact correspondence between linear approximations and non-idempotent intersection types, we develop a general framework for building systems of intersection types characterizing normalization properties. We show how this construction, which uses in a fundamental way Melliès and Zeilberger’s “type systems as functors” viewpoint, allows us to recover equivalent versions of every well known intersection type system (including Coppo and Dezani’s original system, as well as its non-idempotent variants independently introduced by Gardner and de Carvalho). We also show how new systems of intersection types may be built almost automatically in this way.

Game semantics is the art of interpreting types as games and programs as strategies interacting in space and time with their environment. In order to reflect the interactive behavior of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a purely sequential programming language, the program (Player) and its environment (Opponent) will play one after the other, in a strictly alternating way. On the other hand, in the case of a concurrent language, Player and Opponent will be allowed to play several moves in a row, in a non-alternating way. In both cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronize properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this paper, we exhibit a number of simple and fundamental combinatorial structures which ensure that a given scheduling policy encoded as synchronization template defines a symmetric monoidal closed (and in fact ∗-autonomous) bicategory of games, strategies and simulations. To that purpose, we choose to work at a very general level, and illustrate our method by constructing two template game models of linear logic with different flavors (alternating and non-alternating) using the same categorical combinatorics, performed in the category of small categories. As a whole, the paper may be seen as a hymn in praise of synchronization, building on the notion of synchronization algebra in process calculi and adapting it smoothly to programming language semantics, using a combination of ideas at the converging point of game semantics and of categorical algebra

We develop a polarised variant of Curien and Herbelin's lambda-bar-mu-mu-tilde calculus suitable for sequent calculi that admit a focalising cut elimination (i.e. whose proofs are focalised when cut-free), such as Girard's classical logic LC or linear logic. This gives a setting in which Krivine's classical realisability extends naturally (in particular to call-by-value), with a presentation in terms of orthogonality. We give examples of applications to the theory of programming languages. In this version extended with appendices, we in particular give the two-sided formulation of LC with the involutive classical negation. We also show that there is in classical realisability a notion of internal completeness similar to the one of Ludics.

In this paper, we present a modern reformulation of the Dialectica interpretation based on the linearized version of de Paiva. Contrarily to Gödel’s original translation which translated HA into system T, our presentation applies on untyped λ-terms and features nicer proof-theoretical properties. In the Curry-Howard perspective, we show that the computational behaviour of this translation can be accurately described by the explicit stack manipulation of the Krivine abstract machine, thus giving it a direct-style operational explanation. Finally, we give direct evidence that supports the fact our presentation is quite relevant, by showing that we can apply it to the dependently-typed calculus of constructions with universes CCω almost without any adaptation. This answers the question of the validity of Dialectica-like constructions in a dependent setting

ProbNetKAT is a probabilistic extension of NetKAT with a de- notational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to compute effectively in the language. This paper gives an new characterization of ProbNetKAT’s semantics using domain theory, which provides the foundation needed to build a practical implementation. We show how to use the semantics to approximate the behavior of arbitrary ProbNetKAT programs using distributions with finite support. We develop a prototype implemen- tation and show how to use it to solve a variety of problems including characterizing the expected congestion induced by different rout- ing schemes and reasoning probabilistically about reachability in a network

We reformulate the theory of ludics introduced by J.-Y. Girard from a computational point of view. We introduce a handy term syntax for designs, the main objects of ludics. Our syntax also incorporates explicit cuts for attaining computational expressivity. In addition, we consider design generators that allow for finite representation of some infinite designs. A normalization procedure in the style of Krivine’s abstract machine directly works on generators, giving rise to an effective means of computation over infinite designs.
The acceptance relation between machines and words, a basic concept in computability theory, is well expressed in ludics by the orthogonality relation between designs. Fundamental properties of ludics are then discussed in this concrete context. We prove three characterization results that clarify the computational powers of three classes of designs. (i) Arbitrary designs may capture arbitrary sets of finite data. (ii) When restricted to finitely generated ones, designs exactly capture the recursively enumerable languages. (iii) When further restricted to cut-free ones as in Girard’s original definition, designs exactly capture the regular languages.
We finally describe a way of defining data sets by means of logical connectives, where the internal completeness theorem plays an essential role.