From February 10 to February 14, I.S.F.A..
Amphitheater G2 (ground floor).
How to get there . Nearest subway station: stade de Gerland (line B).
Participants are encouraged to submit talk proposals before Dec. 20, 2013 . To do so please send a mail with subject line 'MSC2014:week 5 talk proposal', containing the title and a short text abstract, to the three organizers {patrick.baillot,daniel.hirschkoff,damien.pous}@ens-lyon.fr . We might have to do some selection depending on the number of proposals.
Logic has been since the 1970s a constant source of concepts and methods for the design and study of high-level programming languages. This has in particular enabled the development of functional languages such as Haskell and ML. Among the notions derived from this approach one can cite on the one hand advanced type systems, which allow one to analyse behaviours of programs and guarantee some properties statically, and on the other hand logics for verification, such as Floyd-Hoare logic.
These techniques have initially been developed for sequential programs, but a growing interest has then emerged for concurrent programming, where computation is carried out by processes which communicate and evolve in a non-deterministic way. The concurrent setting has raised new challenges, as the complexity of the new systems makes the task of checking the validity of programs far more difficult. This has in turn led to the development of behavioural theories (contextual equivalences, bisimilarity), and of appropriate techniques to reason on behaviours (coinduction, coalgebraic methods). Again, logic has been a source of inspiration for the design of type systems for concurrent systems, as well as of advanced verification methods, notably in the framework of separation logic. In return, some of the new concepts and techniques have been applied with success to sequential computation.
The goal of this week is to focus on the recent developments and the open questions at the interface beteen logic, programming languages and concurrency theory. It aims at bringing together different viewpoints on the challenges in these area, and to foster in this way interactions between researchers.
last minute changes:
Monday, feb 10 | ||
---|---|---|
9:00-9:15 | Welcome | |
9:15-10:15 | Bas Luttik | Unique Parallel Decomposition |
10:15 | coffee | |
10:30-11:30 | Davide Sangiorgi / Valeria Vignudelli | On the Discriminating Power of Higher-Order Languages |
11:30 Lunch | ||
13:30-14:30 | Yuxin Deng | Open bisimulation for quantum processes |
14:30-15:15 | Daniel Gebler | Compositional specification and metric reasoning on probabilistic nondeterministic systems |
15:15 | coffee | |
15:45-16:30 | Frank Valencia | Epistemic Logic for Concurrency |
Tuesday, feb 11 | ||
---|---|---|
10:00 | coffee | |
10:30-11:30 | Rob Van Glabbeek | Modelling temporal properties of wireless mesh networks |
11:30 Lunch | ||
13:30-14:15 | Dale Miller/Kaustuv Chaudhuri | Formalization of the Bisimulation-Up-To Technique and its Meta Theory |
14:15-15:00 | Sergueï Lenglet | Bisimulations for delimited-control operators |
15:00 | lemon smoothie | |
15:30-16:15 | Nicolas Guénot | Linear Session Types for Solos |
16:30-17:15 | Pawel Sobocinski | Petri nets and compositionality |
Wednesday, feb 12 | ||
---|---|---|
9:00-10:00 | Nobuko Yoshida | Scribble, Runtime Verification and Multiparty Session Types |
10:00 | coffee | |
10:30-11:30 | Frank Pfenning | Concurrent Programming in Linear Type Theory |
11:30 Lunch | ||
13:30-14:15 | Romain Demangeon | Scribble expressiveness: nesting and interrupt |
14:15-15:00 | Jorge Perez | Logic-Based Domain-Aware Session Types |
15:00 | champagne | |
15:30-16:15 | Romain Pechoux | Tiering and non-interference for complexity analysis of imperative and OO programs |
16:15-17:00 | Giovanni Bernardi | Using higher-order contracts to model session types |
20:00 | Social dinner | Restaurant “Le Fleurie”, 123 rue de Gerland directions |
Thursday, feb 13 | Joint day with Chocola seminar - location: ENS Lyon, Monod site - directions | |
---|---|---|
10:00-11:00 | Luke Ong | Functions, Concurrency and Automatic Verification |
11:00 | coffee | |
11:30-12:30 | Gilles Barthe | Verified implementations of cryptographic standards |
12:00 Lunch | ||
14:00-15:00 | Giuseppe Castagna | Polymorphic Functions with Set-Theoretic Types |
15:00-15:30 | sangria |
Friday, feb 14 | ||
---|---|---|
9:00-10:00 | Martin Hofmann | Buchi Types for Infinite Traces and Liveness |
10:00 | coffee | |
10:30-11:30 | Ugo Dal Lago | The Geometry of Synchronization |
11:30 Lunch | ||
13:30-14:15 | Marco Gaboardi | A Core Quantitative Coeffect Calculus |
14:15-15:00 | Damiano Mazza | Linear approximations and Boolean circuits |
15:00-15:30 | caco-calo | |
15:30-16:15 | Pierre Lescanne | Coinduction, Equilibrium and Rationality of Escalation |
* Gilles Barthe Verified implementations of cryptographic standards
* Giovanni Bernardi Using higher-order contracts to model session type
Session types are used to describe and structure interactions between independent processes in distributed systems. Higher-order types are needed to properly structure delegation of responsibility between processes.
In this talk we show that a sublanguage of higher-order web-service contracts provides a fully-abstract model of recursive higher-order session types. The model is set-theoretic, in that the meaning of a contract is the set of contracts with which it complies. The proof of full-abstraction depends on the novel notion of complement of a contract. We show that the new notion lets us type more well-formed programs than the commonly used type duality does, thereby improving existing type systems.
* Giuseppe Castagna 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
* Kaustuv Chaudhuri / Dale Miller Formalization of the Bisimulation-Up-To Technique and its Meta Theory
Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations being computed while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques make defining relations easier and they are increasingly becoming a critical ingredient in the automated checking of bisimilarity. This paper is devoted to the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the pi-calculus (with replication). Our formalization is based on recent work on the proof theory of least and greatest fixpoints, particularly the use of relations defined (co-)inductively, and of coinductive proofs about such relations, as implemented in the Abella theorem prover. An important feature of our formalization is that our definitions of the bisimulation-up-to relations are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. We exploit the existing facilities in Abella for reasoning about objects with binding—such as pi-calculus processes—using lambda-tree syntax and generic reasoning using the nabla-quantifier. (joint work Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller)
* Ugo Dal Lago The Geometry of Synchronization
We incept synchronization into the most concrete model of Girard's Geometry of Interaction, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic with a specific construct modeling synchronization points, and of a multi-token machine model for it. Interestingly, the correctness criterion ensures deadlock freedom for the underlying machine, this way linking logical and operational properties.
* Romain Demangeon Scribble expressiveness: nesting and interrupt
Following Nobuko Yoshida's introduction to Scribble, I present two different (but not unrelated) extensions of the language: nesting and interrupt, and their related theories as session type refinements. Nesting is the ability for a participant in a session to create a private subsession; this mechanism allows users to design modular session types, by extracting subprotocols following a common patterns (such as logins, negotiations, RPCs) from complex specifications and treat them separately. Interrupt is the abilty for a participant to escape from a block of interaction in an exceptional way. Interrupts have to be propagated asynchronously to the other participants. Both extensions use scopes in order to separate a protocol into blocks of interactions.
* Yuxin Deng Open bisimulation for quantum processes
We propose a notion of open bisimulation for quantum processes and show that it provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between quantum processes. We also give a modal characterisation of the behavioural equivalence, by extending the Hennessy-Milner logic to a quantum setting. In addition, we introduce a symbolic semantics and show a coincidence result of symbolic bisimulation and open bisimulation, which paves the way for algorithmic verification of quantum processes. (The talk is based on joint work with Y. Feng and M. Ying)
* Marco Gaboardi A Core Quantitative Coeffect Calculus
Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-linear, reusable data. The latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad.
Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this work, we present a language inspired by a generalized interpretation of the exponential modality. In this language the exponential modality carries a label—an element of a semiring—that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis. (joint work with Aloïs Brunel, Damiano Mazza and Steve Zdancewic)
* Daniel Gebler Compositional specification and metric reasoning on probabilistic nondeterministic systems
Probabilistic transition systems are the fundamental structure in order to provide operational semantics to probabilistic nondeterministic systems and languages. For those systems, boolean notions of behavioural equivalences and logical satisfaction are too fragile. Over the last decade it became clear that metrics measuring degrees of behavioural (bi)similarity and degrees of logical satisfaction are the appropriate notion to allow for robust reasoning. In this talk I will present recent results that characterize an expressive class of probabilistic languages which allows for compositional reasoning. Moreover, I will show how the characterization of those languages is derived from their underlying logical characterization.
* Nicolas Guenot Linear Session Types for Solos
The problem of finding a satisfactory computational interpretation of proofs in linear logic, either in its sequent calculus or proof-nets presentation, has been studied this the inception of this logic, but substantial progress has been made only in the last few years. On one side, the link established between linear formulas and session types has lead to a successful connection between linear logic and concurrent computation, although this approach suffers from several drawbacks. On the other side, proof nets and interaction nets have been used to encode pi-calculus terms but also process calculi without prefixing, such as the solos calculus. The goal of our work is to show how the choice of solos as a basic framework yields a correspondence to linear logic proofs through a form of session types that improves on the current interpretation. In particular, this seems to offer a way towards the definition of a proper ”“Curry-Howard correspondence””, where the many permutations of rules allowed in the sequent calculus would be reflected in the processes as uses of a structural congruence.
* Martin Hofmann Buchi Types for Infinite Traces and Liveness”” (joint work with Wei Chen)
We develop a new type and effect system based on Buchi automata to capture finite and infinite traces produced by programs in a small language which allows non-deterministic choices and infinite recursions. There are two key technical contributions: (a) an abstraction based on equivalence relations defined by the policy Buchi automata, the Buchi abstraction; (b) a novel type and effect system to correctly capture infinite traces. We show how the Buchi abstraction fits into the abstract interpretation framework and show soundness and completeness.
* Serguei Lenglet Bisimulations for delimited-control operators
Control operators allow programs to have access to their execution context. We distinguish abortive operators, such as call/cc, which capture the whole execution context, from delimited-control operators, which capture only a part of the context. Such operators make writing programs with frequent context switches easier (like, for instance, programs with backtracking). In this talk, we present the behavioral theory of the delimited-control operators shift and reset. We propose a definition of contextual equivalence, and different kinds of bisimilarity to characterize it (applicative, normal form, and environmental), each one having its strengths and weaknesses. We also compare contextual equivalence with another form of equivalence over terms based on CPS translation.
* Pierre Lescanne Coinduction, Equilibrium and Rationality of Escalation
Escalation is the behavior of players who play forever in the same game. Such a situation can happen in automatic systems for auction and negotiation as developed in electronic commerce and, tightly associated with infinite games, it is a typical field for application of coinduction which is the tool conceived for reasoning in infinite mathematical structures. In particular, we use coinduction to study formally the game called –dollar auction–, which is considered as the paradigm of escalation. Unlike what is admitted since 1971, we show that, provided one assumes that the other agent will always stop, bidding is rational, because it results in a subgame perfect equilibrium. We show that this is not the only rational strategy profile (the only subgame perfect equilibrium). Indeed if an agent stops and will stop at every step, whereas the other agent keeps bidding, we claim that he is rational as well because this corresponds to another subgame perfect equilibrium. In the infinite dollar auction game, despite of the dogma, the behavior in which both agents stop at each step is not a Nash equilibrium, hence is not a subgame perfect equilibrium, hence is not rational. Happily, the notion of rationality based on coinduction one obtains fits with common sense and experience. Finally the possibility of a rational escalation in an arbitrary game can be expressed as a predicate on games and the rationality of escalation in the dollar auction game can be proved as a theorem. We even check the correctness in the proof in the proof assistant COQ. In this talk we will recall the principles of infinite extensive games, presented in the framework of coinduction, then the concept of equilibrium (Nash equilibrium, subgame perfect equilibrium). We will show how one can prove that the two strategy profiles presented above are equilibria and how this leads to a “rational” escalation in the dollar auction.
* Bas Luttik Unique Parallel Decomposition
A recurring question in process theory is to what extent the behaviours definable in a certain process calculus have a unique decomposition into indecomposable parallel components. Milner and Moller were the first to consider the unique decomposition property in a process calculus for specifying simple finite behaviours. Since then, the property has been re-established several times for different process calculi, each time using a variant of the same proof idea, and most recently for a fragment of the applied pi-calculus. In my talk I will present and discuss an abstract theory of unique decomposition in commutative monoids that is tailored towards application in process theory. I'll explain how the theory can be straightforwardly applied to establish unique parallel decomposition in process calculi modulo strong bisimilarity, and how an adaptation facilitates application in settings modulo weak and branching bisimilarity. I'll conclude with some comments on how to apply the theory to establish unique parallel decomposition in pi-calculi.
* Damiano Mazza Linear approximations and Boolean circuits
The connection between Boolean circuits and certain kinds of linear proof nets has been explored by several people, both in past and recent times (Terui, Mairson, Mogbil, Clément). We recast this correspondence in a broader context, that of the infinitary lambda-calculus, in which linear lambda-terms may be seen as approximations of usual lambda-terms (a closely related framework is that of the resource lambda-calculus, in which finite formal sums of resource lambda-terms approximate usual lambda-terms via the so-called Taylor expansion). The idea emerging in this context is that “linear (or affine, or resource) lambda-terms are to usual lambda-terms what Boolean circuits are to Turing machines”. This perspective allows us to give an alternative, “internal” proof of P-completeness of normalization of the affine lambda-calculus (originally proved by Mairson by encoding Boolean circuits) which is essentially a lambda-calculus restatement of the heart of the Cook-Levin theorem (i.e., “computation is local”). We also present some results using non-uniform lambda-terms (in particular, a type-theoretic characterization of the class P/poly, joint work with Kazushige Terui).
* Luke Ong 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)
* Romain Péchoux Tiering and non-interference for complexity analysis of imperative and OO programs.
A family of type systems based on tiering and non-inteference techniques is introduced in order to control the complexity of imperative and Object Oriented programs. We show that this typing discipline allows us to control extensional and intensional properties of several paradigms including imperative multi-threads, forking processes à la Unix and Java-like languages. In particular, we obtain several characterizations of FPtime and FPspace for typable programs under some restrictions (termination, confluence, strong normalization, safety). We also show that type inference is decidable in polynomial time for all these type systems.
* Jorge Perez Logic-Based Domain-Aware Session Types
Software services and governing communication protocols are increasingly domain-aware. Domains can have multiple interpretations, such as the principals on whose behalf processes act or the location at which parties reside. Domains impact protocol compliance and access control, two central issues to overall functionality and correctness in distributed systems. This paper proposes a session-typed process framework for domain-aware communication-centric systems based on a Curry- Howard interpretation of linear logic, here augmented with nom- inals from hybrid logic indicating domains. These nominals are explicit in the process expressions and govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics for modal logic. Flexible access relationships among domains can be elegantly defined and statically enforced. The framework can also account for scenarios in which domain information is discovered only at runtime.
Due to the logical origins of our systems, well-typed processes enjoy session fidelity, global progress, and termination. Moreover, well-typed processes always respect the accessibility relation and satisfy a form of domain parametricity, two properties crucial to show that domain-related properties of concrete programs are satisfied. (joint work with Luís Caires, Frank Pfenning, and Bernardo Toninho)
* Frank Pfenning “Concurrent Programming in Linear Type Theory
Over the last few years we have pursued a research program to provide a foundation for session-typed, message-passing concurrency via a Curry-Howard interpretation of (intuitionistic) linear logic. We introduce the programming language emerging from this effort, mostly by means of a variety of example programs. We also briefly discuss our current research on foundational as well as pragmatic issues surrounding this language. [Joint work with Luis Caires, Bernardo Toninho, Jorge Perez (Universidade Nova de Lisboa) and Elsa Gunter, Dennis Griffith (University of Illinois at Urbana-Champaign)]
* Davide Sangiorgi and Valeria Vignudelli On the Discriminating Power of Higher-Order Languages
* Pawel Sobocinski Petri nets and compositionality
I will give an overview of recent work on a compositional algebra of Petri nets, focussing on behavioural equivalence, algebraic properties and applications to model checking.
* Frank Valencia Epistemic Logic for Concurrency
* Rob van Glabbeek Modelling temporal properties of wireless mesh networks
In the study of wireless mesh networks, I want to formulate a property that says that under certain conditions a packet submitted by a source node will eventually be delivered at the destination. The best framework to formalise such a property Phi in appears to be LTL, Linear-time Temporal Logic. And getting the side-conditions right is non-trivial. In order for Phi to have any chance of holding, I need to assume three properties of the system on which Phi is interpreted: progress, justness and (weak) fairness. I will explain the difference between these properties, and how all three are needed here. The case study of wireless mesh networks is just for motivation; it supports design decisions leading to a model of concurrency that consists of a labelled transition system together with a set of valid infinite traces (described in LTL). Going back to the case study of wireless networks, in order for Phi to hold in a process algebraic model, one needs a non-lossy broadcast mechanism. Finally, Phi turns out not to hold for common routing protocols like AODV.
* Nobuko Yoshida Scribble, Runtime Verification and Multiparty Session Types
We give a summary of our recent research developments on multiparty session types, and our collaborations with industry partners (Red Hat, Cognizant and VMware) and a major, long-term, NSF-funded project (Ocean Observatories Initiatives) to provide an ultra large-scale cyberinfrustracture (OOI CI) for 25-30 years of sustained ocean measurements to study climate variability, ocean circulation and ecosystem dynamics. We shall first talk how Robin Milner, Kohei Honda and Yoshida started collaborations with industry to develop a web service protocol description language called Scribble and discovered the theory of multiparty session types through the collaborations. We then talk about the recent developments in Scribble and the runtime session monitoring framework currently used in the OOI CI.