Séminaire, Feb. 13, 2014


La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi B. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.


10:00 – 11:00
Luke Ong (Oxford University)

We study the automatic verification of asynchronous message-passing concurrent programs. This talk will begin with a survey of a recent project [1], Soter, to verify safety properties of Erlang programs by abstract interpretation and infinite-state model checking, and a discussion of the lessons learn. The rest of the talk will focus on an approach to address a source of imprecision of the Soter approach. We study the reachability problem of concurrent pushdown systems that communicate via unbounded and unordered message buffers, a model of computation for Erlang programs. Our goal is to relax the common restriction that messages can only be retrieved by a pushdown process when its stack is empty. We introduce a new class of Asynchronously Partially Commutative Pushdown Systems with a mild shape constraint on the stacks for which the coverability problem is decidable. Stacks that fit the shape constraint may reach arbitrary heights; further a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. This class extends previous computational models studied in the setting of asynchronous procedural calls, and enables the safety verification of a large class of recursively-defined message-passing programs. This is joint work with Jonathan Kochems and Emanuele D'Osualdo. [1] [1]http://mjolnir.cs.ox.ac.uk/soter

11:30 – 12:30
Gilles Barthe (IMDEA (Madrid))
14:00 – 15:00
Giuseppe Castagna (CNRS - Univ. Paris Diderot (Paris 7))

We present a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). In a first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed lambda-calculus with intersection types and an efficient evaluation model for it. In the second part, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations. This work provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.