Séminaire, 13 février 2014

Programme

10:00 – 11:00

Luke Ong (Oxford University)

Invited talk: Functions, Concurrency and Automatic Verification

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))

Invited talk: Verified implementations of cryptographic standards

14:00 – 15:00

Giuseppe Castagna (CNRS - Univ. Paris Diderot (Paris 7))

Invited talk: Polymorphic Functions with Set-Theoretic Types

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.