Paper Presentation

MSO

We consider a class of infinite two-player games on finitely coloured graphs. Our main question is: given a winning condition, what is the inherent blow-up (additional memory) of the size of the I/O automata realizing winning strategies in games with this condition. This problem is rel- evant to synthesis of reactive programs and to the theory of automata on infinite objects. We provide matching upper and lower bounds for the size of memory needed by win- ning strategies in games with a fixed winning condition. We also show that in the general case the LAR (latest appear- ance record) data structure of Gurevich and Harrington is optimal. Then we propose a more succinct way of repre- senting winning strategies by means of parallel composi- tions of transition systems. We study the question: which classes of winning conditions admit only polynomial-size blowup of strategies in this representation.

We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah us- ing set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We discuss some applications of the result concerning unambiguous tree automata and definability of winning strategies in infinite games. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory.

We study definability and complexity issues for automatic and ω-automatic structures. These are, in general, infinite structures but they can be finitely presented by a collection of automata. Moreover, they admit effective (in fact auto- matic) evaluation of all first-order queries. Therefore, au- tomatic structures provide an interesting framework for ex- tending many algorithmic and logical methods from finite structures to infinite ones. We explain the notion of (ω-)automatic structures, give examples, and discuss the relationship to automatic groups. We determine the complexity of model checking and query evaluation on automatic structures for fragments of first- order logic. Further, we study closure properties and de- finability issues on automatic structures and present a tech- nique for proving that a structure is not automatic. We give model-theoretic characterisations for automatic structures via interpretations. Finally we discuss the composition the- ory of automatic structures and prove that they are closed under finitary Feferman-Vaught-like products.

We consider the logic mso+u, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the mso+u theory of (N, ≤) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.

System F and second-order logic

The problems of typability and type checking exist for the Girard/Reynolds second-order polymorphic typed /spl lambda/-calculus (also known as “system F”) when it is considered in the “Curry style” (where types are derived for pure  lambda-terms). Until now the decidability of these problems for F itself has remained unknown. We first prove that type checking in F is undecidable by a reduction from semi-unification. We then prove typability in F is undecidable by a reduction from type checking. Since the reduction from typability to type checking in F is already known, the two problems in F are equivalent (reducible to each other). The results hold for both the usual lambda-K-calculus and the more restrictive lambda-I-calculus.

We give two proofs of strong normalization for second order classical natural deduction. The first one is an adaptation of the method of reducibility candidates introduced in [9] for second order intuitionistic natural deduction; the extension to the classical case requires in particular a simplification of the notion of reducibility candidate. The second one is a reduction to the intuitionistic case, using a Kolmogorov translation.

The polymorphic, or second-order, typed lambda calculus is an extension of the typed lambda calculus in which polymorphic functions can be defined. In this paper, we will prove that the standard set-theoretic model of the ordinary typed lambda calculus cannot be extended to model this language extension.

Lecture notes of a PhD course on classical realizability.

This paper is a study of the forcing translationthrough the proofs as programs correspondence in classicallogic, following the methodology introduced by Krivine in [12],[14]. For that, we introduce an extension of (classical) higher-orderarithmetic suited to express the forcing translation, calledPAω+. We present the proof system of PAω+ based on Curry-styleproof terms with call/cc as well as the correspondingclassical realizability semantics. Then, given a poset of conditions(represented in PAω+ as an upwards closed subset of a fixed meetsemi-lattice), we define the forcing translation A |→ (p A)(where A ranges over propositions) and show that the correspondingtransformation of proofs is induced by a simpleprogram transformation t |→ t* defined on raw proof-terms(i.e. independently from the derivation). From an analysis ofthe computational behavior of transformed programs, we showhow to avoid the cost of the transformation by introducingan extension of Krivine's abstract machine devoted to theexecution of proofs constructed by forcing. We show that thismachine induces new classical realizability models and presentthe corresponding adequacy results.

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.

Mu-calculus and fixed-points of types

The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call μMALL=, satisfies two fundamental proof theoretic properties. In particular, μMALL= satisfies cut-elimination, which implies consistency, and has a complete focused proof system. This second result about focused proofs provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We then consider applying these two results about μMALL= to derive a focused proof system for an intuitionistic logic extended with induction and co-induction. The traditional approach to encoding intuitionistic logic into linear logic relies heavily on using the exponentials, which unfortunately weaken the focusing discipline. We get a better focused proof system by observing that certain fixed points satisfy the structural rules of weakening and contraction (without using exponentials). The resulting focused proof system for intuitionistic logic is closely related to the one implemented in Bedwyr, a recent model checker based on logic programming. We discuss how our proof theory might be used to build a computational system that can partially automate induction and co-induction. (Note: One shall also look at the journal long version (https://www.cs.utexas.edu/users/tocl/a/427baelde.pdf) but only to compare the cut-elimination proof in the conference and the journal version, no need to go deeper!)

Modal μ-calculus is one of the central logics for verification. In his seminal paper, Kozen proposed an axiomatization 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 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.

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 variant 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 programs. 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.