5th meeting: November 19, 2010, at ENS Lyon

* 5th meeting of the COMPLICE project *

Date : Friday, November 19th 2010.

Location : LIP, ENS de Lyon, Amphi B, 3rd floor.

Access instructions (Enter at 46 allée d’Italie, that is to say below the big "arch"; there is a reception desk)

Access map

Invited speaker: Martin Hofmann (Munich)

Preliminary programme:

Abstracts:

 Alois Brunel (Paris 13). A biorthogonality-based realizability for time and space complexity

Dal Lago & Hofmann have introduced some years ago a realizability framework, allowing uniform proofs of the soudness of various type systems (like LAL, EAL, LFPL, ...) with respect to certain time complexity classes. The crucial point is that with every realizer comes an element of a resource monoid that represents a time bound.

Following their methodology, we propose a new framework built around the notions of observable and orthogonality between programs and environments, which is strongly related to the Krivine classical realizability.

It allows us to express both time and space properties of programs within a single framework. As an example, we will apply this technique to obtain a semantic proof of the soundness w.r.t PSPACE of the recent type system STA_B introduced by Gaboardi, Marion & Ronchi Della Rocca.

 Hugo Feree (stage à Nancy). Polynomial interpretation of stream programs.

We define a new notion of polynomial time complexity for type 2 functions, which makes more sense for functions over streams than the the one of Basic Feasible Functions. (This definition can also be justified using computable real functions. Indeed, the lasts can be seen as type 2 functions, and it turns out that the usual recursive analysis definition of polynomial time computable real functions matches our definition.) The interpretation of type-1 programs as polynomials has already allowed to characterise PTIME (or non size increasing) functions. We describe a basic Haskell-like stream language and use order 2 polynomial interpretations to characterise in the same way polynomial time type 2 functions as we defined them. As a corollary, we can get a similar characterisation of BFF functionals.

 Lucien Capdevielle (stage Lyon). Light types for polynomial space computation in lambda-calculus.

We present a polymorphic type system for lambda calculus ensuring that well- typed programs can be executed in polynomial space: dual light a-ne logic with booleans (DLALB). To build DLALB we start from DLAL which has a simple type language with a linear and an intuitionistic type arrow, and one modality and which characterize FPTIME functions. In order to extend its expressivity we add two boolean constants and a conditional constructor in the same way that has been done with the system STAB by Gaboardi-Marion-Ronchi Della Rocca. We show that the value of a well-typed term can be computed by an alternating machine in polynomial time, thus such term represents a program of PSPACE (given that PSPACE = APTIME ). We also prove that all polynomial space decision functions can be represented in DLALB. Therefore DLALB characterizes PSPACE predicates.

 Martin Hofmann (Munich) (invité). Title: Amortized resource analysis

Abstract: resource analysis aims at automatically determining and upper bound on the resource usage of a program as a function of its input size. Resources in this context can be runtime, heap- and stack size, number of occurrences of certain events, etc.

The amortized approach to resource analysis works by associating "credits" with elements of data structures and to "pay" for each consumption of resource from the credits currently available. In this way composite programs and programs with intermediate data structures can be analysed more conveniently than would otherwise be the case.

Amortization was introduced by Tarjan in the 70s in the context of manual complexity analyis of algorithms. More recently, it has been used for type-based automatic resource analysis.

The talk describes the key concepts with simple examples and then moves on to recent work on the inference of multivariate polynomial resource bounds for functional programs (joint work with Jan Hoffmann and Klaus Aehlig to appear at POPl2011).

 Roberto M. Amadio, Nicolas Ayache, Yann Régis-Gianas , Ronan Saillard. Certifying cost annotations in compilers

We discuss the problem of building a compiler which can lift in a provably correct way pieces of information on the execution cost of the object code to cost annotations on the source code. To this end, we need a clear and flexible picture of: (i) the meaning of cost annotations, (ii) the method to prove them sound and precise, and (iii) the way such proofs can be composed. We propose a so-called labelling approach to these three questions. As a first step, we examine its application to a toy compiler. This formal study suggests that the labelling approach has good compositionality and scalability properties. In order to provide further evidence for this claim, we report our successful experience in implementing and testing the labelling approach on top of a prototype compiler written in OCAML for (a large fragment of) the C language.

 Tobias Heindel (Paris 13). Church-Rosser in Derived LTSs with True Concurrency

The central idea of this talk is a general technique that takes a set of rewriting rules as input and derives a behavioral congruence that also takes aspects of true concurrency into account and thus allows to make finer distinctions than "standard" behavioral equivalences. The theory is developed in the setting of adhesive categories and based on the work by Ehrig and Kö̈nig on borrowed contexts, which provides a variation of label derivation à la Leifer and Milner. In general, the automatic derivation of LTSs from rewriting systems might help to pinpoint the fundamental differences between the lambda calculus and the pi-calculus and thus might be relevant to implicit complexity for process calculi.

 Hugo Feree (stage à Nancy). Polynomial interpretation of stream programs.

We define a new notion of polynomial time complexity for type 2 functions, which makes more sense for functions over streams than the the one of Basic Feasible Functions. (This definition can also be justified using computable real functions. Indeed, the lasts can be seen as type 2 functions, and it turns out that the usual recursive analysis definition of polynomial time computable real functions matches our definition.) The interpretation of type-1 programs as polynomials has already allowed to characterise PTIME (or non size increasing) functions. We describe a basic Haskell-like stream language and use order 2 polynomial interpretations to characterise in the same way polynomial time type 2 functions as we defined them. As a corollary, we can get a similar characterisation of BFF functionals.