# 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.

## Visitors

04 Mar 30 Apr 2019 Ø18-511a-2

Fabrizio Montesi , Marco Peressotti

Permalink

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

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

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 visited the CL group at IMADA and to give the seminar Composable Open Memory Transactions .

## Seminars

University of Glasgow, United Kingdom

Wed 29 Jan 2020 at 14:15 IMADA seminar room Abstract Permalink

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

Concurrency and Logic research group

Fri 17 Jan 2020 at 12:30 IMADA meeting room Abstract Permalink

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.

Concurrency and Logic research group

Fri 11 Jan 2019 at 10:30 IMADA meeting room Abstract Permalink

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.

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.

Concurrency and Logic research group

Fri 25 May 2018 at 10:30 IMADA meeting room Abstract Permalink

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

Concurrency and Logic research group

Fri 20 Apr 2018 at 10:30 IMADA meeting room Abstract Permalink

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.

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.

Warsaw University of Technology, Poland

Tue 27 Jun 2017 at 14:15 IMADA seminar room Abstract Permalink

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.

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.