2nd meeting: 8 june 2009, at ENS Lyon

* 2nd meeting of the COMPLICE project *

Date : Monday, June 8th 2009.

Location : LIP, ENS de Lyon, Amphi B, 3e étage.

Access instructions

Access map

Programme

Résumés:

*Roberto Amadio: On stratified regions

Type and effect systems are a tool to analyse statically the behaviour of programs with effects. We present a proof based on the so called reducibility candidates that a suitable stratification of the type and effect system entails the termination of the typable programs. The proof technique covers a simply typed, multi-threaded, call-by-value lambda-calculus, equipped with a variety of scheduling (preemptive, cooperative) and interaction mechanisms (references, channels, signals). technical report

* Hamza Hajji: Implicit Complexity and certificate synthesis, a glimpse

Program complexity analysis deals with: values growth, time of execution, etc. It consists in defining formal methods that aims at characterizing these properties, and notably meant to be implemented at the end.

I present a method for detecting polynomial-time programs. The method is based on the mwp-polynomials of Kristiansen and Jones, refined by Ben-Amram, Kristiansen and Jones in order to keep more details on the data flow.

This method is intensionally complete for Ptime on a toy language where tests are replaced by non-deterministic choices. I will also discuss some issues concerning implementation.

*Ulrich Schöpp: Functional Programming in Sublinear Space (joint work in progress with Ugo Dal Lago)

We are studying how programming in sublinear space can be supported by specifically designed programming languages. Writing programs with sublinear space usage often requires one to use special implementation techniques for common tasks. For example, one cannot compose two functions directly, as there may not be enough space for the intermediate result, but must instead compute and recompute small parts of the intermediate result on demand. Since such techniques are sometimes hard to handle, we are aiming to design a programming language that makes such techniques transparent and allows one to write programs in a more natural way.

This talk will be about an approach to developing a functional programming language for sublinear space. The approach is based on modelling computation by interaction in the style of particle style Geometry of Interaction. Following a semantic approach, we derive a functional programming language from the closely-related Int-construction, which allows one to study interactive computation on the basis of a given functional language. The proposed functional language is formulated by means of a type system inspired by Barber & Plotkin’s Dual Linear Logic and Baillot & Terui’s Dual Light Affine Logic. In order to assess the intensional expressiveness of the language, we implement in the language Moeller-Neergaard & Mairson’s algorithm for sublinear space iteration by computational amnesia.