Seminars & Visitors

The Artificial Intelligence, Cybersecurity, and Programming Languages 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, ACP seminars are held every Friday at 12:30 in IMADAs møderum 2, 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 ACP seminars and on the right the researchers that visited ACP group.


Zesen Qian
Aarhus University, Denmark
01 Sep 31 Dec 2021 Ø18-511a-2
Fabrizio Montesi , Marco Peressotti
Ornela Dardha
University of Glasgow, United Kingdom
27 Jan 30 Jan 2020 Ø16-601a-2
Jacopo Mauro
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 New Linear Logic for Deadlock-Free Session-Typed Processes

The π-calculus, viewed as a core concurrent programming language, has been used as the target of much research on type systems for concurrency. In this paper we propose a new type system for deadlock- free session-typed π-calculus processes, by integrating two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom by forbidding cyclic process connections. The second is Kobayashi’s approach in which types are annotated with priorities so that the type system can check whether or not processes contain genuine cyclic dependencies between communication operations. We combine these two techniques for the first time, and define a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities. This can be seen in three ways: (i) as a new linear logic in which cyclic structures can be derived and a Cycle-elimination theorem generalises Cut-elimination

Hypothetical answers to continuous queries over data streams

Continuous queries over data streams often delay answers until some relevant input arrives through the data stream. These delays may turn answers, when they arrive, obsolete to users who sometimes have to make decisions with no help whatsoever. Therefore, it can be useful to provide hypothetical answers - “given the current information, it is possible that X will become true at time t” - instead of no information at all. In this talk we present a semantics for queries and corresponding answers that covers such hypothetical answers, together with an online algorithm for updating the set of facts that are consistent with the currently available information.

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
Saverio Giallorenzo
Concurrency and Logic research group
Fri 29 Jun 2018 at 10:30 IMADA meeting room Abstract Permalink

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.