## The pi-calculus and Logics for Concurrent and Sequential Programs

Kohei Honda

Queen Mary University of London

Abstract:This talk is about how we can represent computational behaviour with a mathematical rigor and uniformity, and how such representation can be useful for their high- level specifications and reasoning. Diverse software behaviours can be found on our PCs, on Internet and the web. A perhaps surprising fact is that all of these behaviour can be represented faithfully in a small calculus of name passing, the pi-calculus, up to some abstraction. Related with other semantic theories such as game semantics and Linear Logic, the calculus can represent diverse computational behaviour with precision, sequential and concurrent, stateless and stateful, shared variable and message passing, first-order and higher-order, coupled with its rich theories of types. In this talk, we shall discuss why such representation is possible and what they can give us, drawing from our experience so far on its applications to logical validation of a wide range of programming languages, taking examples from typed business protocols, imperative programs and higher-order functions. The logic, which is the classical Hennessy-Milner Logic applied to typed processes, allows reasoning about processes through proof systems for what correspond to partial and total correctness through its two proof systems, characterising respectively the standard May and Must preoder: their mixture gives a proof system which characterises bisimilarity. The logic allows compositional reasoning for diverse classes of process behaviour, including typed communicating processes and first-order and higher-order programs, which will be illustrated through examples. The logic can embed assertions and proof rules of the program logics including Hoare logic for imperative programs and its various extensions.

Where:6.3.5When:Wednesday, April 22 2009Time:11:00## A reconstruction of session types in a linear pi calculus

Vasco T. Vasconcelos

FCUL

Abstract:We present a reconstruction of session types in a linear pi calculus where types are qualified as linear or unrestricted. Linearly qualified communication channels are guaranteed to occur in exactly one thread, possibly multiple times. In our language each channel is characterised by two distinct variables, one used for reading, the other for writing; scope restriction binds together two variables, thus establishing the correspondence between the two ends of a same channel. This mechanism allows a precise control of resources via a linear type system. We build the language gradually, starting from simple input/output, then adding choice, recursive types, replication and finally subtyping. We also present an algorithmic type checking system.

Where:6.3.5When:Wednesday, April 8 2009Time:11:00## Services: when specification meets implementation

Luís Cruz-Filipe

FCUL

Abstract:Within the Sensoria project, several approaches have been proposed to the design, modelling and implementation of service-oriented systems. These approaches stem from different motivations, different perspectives and different levels of abstraction, and have different goals in mind; however, the object of their study is the same, and as such they often share several non-trivial common features below the surface.

This talk focuses on two languages and the concepts they share. On a higher level, SRML is a modelling language aimed at supporting the more abstract levels of design specification (‘business modelling’). On a lower level, the Conversation Calculus models services as processes that can be analyzed using techniques from process calculus. We will show that these two approaches end up sharing a significant number of concepts, and establish a relationship between CC processes and SRML specifications that not only highlights these similarities, but also provides more powerful tools for analyzing and studying properties of these systems.

Where:6.3.5When:Wednesday, April 1 2009Time:11:00## Bring Models Closer to Code

Oscar Nierstrasz

University of Bern

Abstract:There is often a huge gap between domain models and software source code. Features and other domain concepts are hard to identify in source code. The run-time architecture of an application can be hard to reconcile with static source organization. Domain Specific Languages partially help to close this gap, but they are often disconnected from the tools that support the host language. We describe two projects that attempt to bring models closer to code.

(i) Diesel is a lightweight language workbench to develop DSLs that are tightly integrated with the host language and the associated development tools. Aspects are used to adapt the model of the host language towards that of a DSL and to modularly scope language transformations in the DSL code.

(ii) Hermion is an integrated development environment that integrates dynamic information with the conventional static source views to better guide the developer. The correlation, for example, between run-time features and the software components that support them, is thus exposed to the developer.

(The talk will be accompanied with demos of this work-in-progress)

Where:6.3.5When:Wednesday, March 25 2009Time:11:00## Really Linear Types for the Pi-Calculus

Luís Caires

UNL

Abstract:Don't miss this talk if you are interested in type theory (for concurrency), linear logic, name passing models of computation, and realizability semantics.

Where:6.3.5When:Wednesday, March 18 2009Time:11:00## Adaptive event-based systems for heterogeneous networks

Boris Koldehofe

Universität Stuttgart

Abstract:An increasing number of applications, for instance business applications like logistic chains, integrate data from a large number of data sources. This trend is amplified by the fact that in the future the number of sensor devices is expected to grow to possibly billions or trillions of devices. In this context event-based communication plays an important role to i) integrate and process this information effectively, ii) allow for simple reconfiguration of applications. This talk discusses research challenges as well as adaptation strategies in realizing adaptive event-based systems that can be deployed in heterogeneous networks. In particular, we focus on two main classes of event-based systems, publish/subscribe and complex event processing. The first allows asynchronous interactions between senders and the receivers, while the latter also supports the detection of complex situations by performing correlations between events.

Where:6.3.5When:Wednesday, March 11 2009Time:11:00## Safe and authorized resource usage on open networks

Neva Slani

FCUL

Abstract:We define a problem of safe and authorised resource usage in what we say are open networks. As a solution we propose a process calculus model with a type system enabling resource access control. By open network is meant one that is only partially known (i.e. its data, locations, resources, etc) at compile-time. For reaching that final model we divide the construction in phases, analysing first the problem in a concurrent context, before passing to a distributed one. A special attention is given to types and type systems, since those guarantee the desired safety properties: as first safe usage, and then authorised usage for the resources at locations inside of a known part of the network. As we do not assume total knowledge of the network, the presented mechanism involves both static and dynamic type-checking, trying to enefit as much from the first.

Where:6.3.5When:Wednesday, January 28 2009Time:11:00## The intuitionistic logical words "absurdum", "or" and "there exists" are not etched on tablets of stone

Fernando Ferreira

FCUL

Abstract:The rules of elimination of the connectives "absurdum", "or" and "there exists" have been subjected to some criticism because they are not as natural and as well behaved as the other inferential rules. In fact, Jean-Yves Girard says that "the elimination rules [of these connectives] are very bad". Moreover, in order to have normal proofs with the subformula property, there is the need to add some ad hoc conversions: the commuting conversions. Girard adds that "the need to add these supplementary rules reveals an inadequacy of the syntax". We present an embedding of the intuitionistic predicate calculus into a second-order predicative system with no "bad" connectives. Moreover, in join work with Gilda Ferreira, we show that the redex and the conversum of a commuting conversion of the original calculus translate into equivalent derivations by means of a series of bidirectional applications of standard conversions.

Where:6.3.5When:Wednesday, January 14 2009Time:11:00## Model-Based Testing

Ana Paiva

FEUP

Abstract:Model-based testing (MBT) is a software testing technique in which test cases are derived from a model of the system under test (SUT). It allows checking the conformity between the implementation and the model of the SUT, introducing more systematization and automation into the testing process. This presentation describes how MBT fits into a typical software life cycle and how it differs from other testing approaches. It also discusses issues related with the construction of the SUT model, such as the choice of the right level of abstraction, presents different test coverage criteria according to the characteristics of the modelling notation and techniques to fill the gap between abstract and concrete test cases to automate execution. Finally, a model-based testing tool (Spec Explorer) will be used to illustrate the theoretical concepts.

Where:6.3.5When:Wednesday, January 14 2009Time:11:00## Fully compressed Sufix Trees

Luís Russo

IST

Abstract:Suffix trees are by far the most important data structure in stringology, with myriads of applications in fields like bioinformatics and information retrieval. Classical representations of suffix trees require O(n \log n) bits of space, for a string of size n. This is considerably more than the n \log_2\sigma bits needed for the string itself, where \sigma is the alphabet size. The size of suffix trees has been a barrier to their wider adoption in practice. Recent compressed suffix tree representations require just the space of the compressed string plus \Theta(n) extra bits. This is already spectacular, but still unsatisfactory when \sigma is small as in DNA sequences.

In this talk we introduce the first compressed suffix tree representation that breaks this linear-space barrier. Our representation requires sublinear extra space and supports a large set of navigational operations in logarithmic time. An essential ingredient of our representation is the lowest common ancestor (LCA) query. We reveal important connections between LCA queries and suffix tree navigation.Where:6.3.5When:Wednesday, June 25 2008Time:11:00