Seminars & Visitors

The Concurrency and Logic group organises weekly meetings, frequently in the form of public seminars, with the aim of presenting and discussing ongoing research. Seminars are mainly in the domain (but not limited to) concurrency, logic, programming languages, type theory, proofs, and software engineering.

Unless differently indicated, CL seminars are held every Friday at 10:30 in IMADAs møderum, SDU, Odense. The seminars’ schedule is managed by Luís Cruz-Filipe and is also available as an ics feed.

The calendar below reports on the left the schedule of the CL seminars and on the right the researchers that visited CL group.


Eros Fabrici
University of Udine, Italy
04 Mar 26 Jun 2019 Ø18-511a-2
Fabrizio Montesi
Wen Kokke
University of Edinburgh, United Kingdom
04 Mar 30 Apr 2019 Ø18-511a-2
Fabrizio Montesi , Marco Peressotti
Isabel Nunes
University of Lisbon, Portugal
11 Feb 15 Feb 2019 Ø16-601a-2
Luís Cruz-Filipe
Stefano Pio Zingaro
University of Bologna, Italy
01 Oct 2018 27 Jan 2019 Ø18-511a-2
Fabrizio Montesi

Stefano Pio Zingaro will work jointly with Saverio Giallorenzo and Fabrizio Montesi, focusing on Service Oriented Computing for Cloud and Embedded Systems.

Jacopo Mauro
Oslo University, Norway
30 Oct 2017
Fabrizio Montesi

Jacopo Mauro visited the CL group at IMADA and to give the seminar Application Deployment - What can be automated?.

Tomasz Brengos
Warsaw University of Technology, Poland
25 Jun 05 Jul 2017 Ø18-511a-2
Marco Peressotti

Tomasz Brengos visited Marco Peressotti to conduct research on the behavioural theory of timed and Büchi automata and to give the seminar A uniform framework for tiemd automata.

Marco Peressotti
University of Udine, Italy
18 Jan 2017
Fabrizio Montesi

Marco Peressotti visited the CL group at IMADA and to give the seminar Composable Open Memory Transactions .


A fully-abstract semantics for Classical Processes

We present Hypersequent Classical Processes (HCP), a revised interpretation of the “Proofs as Processes” correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the π-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by ⊗ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the π-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini’s theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.

Applied Choreographies

Implementations of choreographic models use message routing technologies distant from their related theoretical models (e.g., CCS/π channels). This drives implementers to mediate discrepancies with the theory through undocumented, unproven adaptations, weakening the reliability of their implementations. We present a framework of Applied Choreographies (AC) where programmers write choreographies in a language that follows the standard syntax and semantics of previous works. Then, choreographies are compiled to a real-world execution model for Service-Oriented Computing (SOC). To manage the complexity of this task, our compilation happens in three steps, respectively dealing with: implementing name-based communications using the concrete mechanism found in SOC, projecting a choreography to a set of processes, and translating processes to a distributed implementation in terms of services.

Introduction seminar on previous work and research interests

Presentation to the Concurrency and Logic group, covering previous work on Constraint Programming and portfolio solvers, Cloud deployments, and DevOps practices.

Connectors Meet Choreographies

Presentation of Cho-Reo-graphies (CR), a model where choreographies are parametric in the (Reo) connectors through which parties communicate. CR is the first choreography model where different communication semantics (e.g., synchronous and asynchronous) can freely be mixed in the same choreography. We prove that if a choreography respects the rules of the connectors that it uses, then the process implementation that we can synthesise from it enjoys deadlock freedom.

Application Deployment - What can be automated?

In modern software systems, deployment is an integral and critical part of application development. A natural question arises: to what extent can we automate the deployment of complex, distributed, and scalable software systems? In the first part of this talk, we will try to give an answer to this question providing some insights on the complexity of the problems of dealing with application deployment and describing tools that can be used. We then describe a recent approach to take into account deployment at the modeling level, thus allowing to perform deployment conscious decisions during the early stages of a system development.

A uniform framework for timed automata

Timed automata, and machines alike, currently lack a general mathematical characterisation. We introduce a uniform coalgebraic understanding of these devices. This framework encompasses known behavioural equivalences for timed automata and paves the way for the extension of these notions to new timed behaviours and for the instantiation of established results from the coalgebraic theory as well. Lax functors are the cornerstone of the framework: they allow us to model time flow as a context property and hence offer a general and expressive setting where to study timed systems. In this setting the index category encodes “how step sequences form executions” (e.g. whether steps duration is accumulated or kept distinct) whereas the base category encodes “step nature and composition” (e.g. non-determinism and labels). Finally, we develop the notion of general saturation for lax functors and show how equivalences of interest for timed behaviours are instances of this notion. This characterisation allows us to reason about the expressiveness of said notions within a uniform framework and organise them in a spectrum independent from the behavioural aspects encoded in the base category.

Composable Open Memory Transactions

Transactional memory (TM) has emerged as a promising high-level concurrency control mechanism alternative to fine grained lock-based synchronization. However, most TM models admit only isolated transactions, which are not adequate in multi-threaded programming where transactions have to interact via shared data before committing. We present Open Transactional Memory (OTM), a programming model supporting safe, data-driven interactions between composable memory transactions. In this model, different transactions are transparently merged at runtime as soon as they access to shared variables; their threads can then cooperate, until they all either commit or abort together. Thus, this model relaxes the isolation requirement still guaranteeing atomicity; moreover, it allows for loosely-coupled interactions since transaction merging is dynamic and driven only by accesses to shared data, with no need to specify participants beforehand. We present OTM in the setting of the Haskell language, taking advantage of its type system for guaranteeing composability.