25 citations · 59 across the 17 of their papers we have counts for
19 papers
Multiparty Session Types with a Bang!
Matthew Alan Le Brun, Simon Fowler, Ornela Dardha
Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. In this paper we explore the implications of including type-level replic…
MAG!: The Role of Replication in Typing Failure-Prone Communication
Matthew Alan Le Brun, Ornela Dardha
MAG is a Multiparty, Asynchronous and Generalised -calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type sy…
Session Types for the Transport Layer: Towards an Implementation of TCP
Samuel Cavoj, Ivan Nikitin, Colin Perkins +1
Session types are a typing discipline used to formally describe communication-driven applications with the aim of fewer errors and easier debugging later into the life cycle of the…
EXPRESSing Session Types
Ilaria Castellani, Ornela Dardha, Luca Padovani +1
To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard -calculus by means of a sui…
Traced Types for Safe Strategic Rewriting
Rongxiao Fu, Ornela Dardha, Michel Steuwer
Strategy languages enable programmers to compose rewrite rules into strategies and control their application. This is useful in programming languages, e.g., for describing program…
Structural Subtyping as Parametric Polymorphism
Wenhao Tang, Daniel Hillerström, James McKinna +4
Structural subtyping and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider rec…
MAG: Types for Failure-Prone Communication
Matthew Alan Le Brun, Ornela Dardha
Multiparty Session Types (MPST) are a typing discipline for communication-centric systems, guaranteeing communication safety, deadlock freedom and protocol compliance. Several work…
Proceedings Combined 28th International Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics
Ornela Dardha, Valentina Castiglioni
This volume contains the proceedings of EXPRESS/SOS 2021: the Combined 28th International Workshop on Expressiveness in Concurrency and the 18th Workshop on Structural Operational…
Papaya: Global Typestate Analysis of Aliased Objects Extended Version
Mathias Jakobsen, Alice Ravier, Ornela Dardha
Typestates are state machines used in object-oriented programming to specify and verify correct order of method calls on an object. To avoid inconsistent object states, typestates…
Multiparty Session Types for Safe Runtime Adaptation in an Actor Language (Extended version)
Paul Harvey, Simon Fowler, Ornela Dardha +1
Human fallibility, unpredictable operating environments, and the heterogeneity of hardware devices are driving the need for software to be able to adapt as seen in the Internet of…
Separating Sessions Smoothly
Simon Fowler, Wen Kokke, Ornela Dardha +2
This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and stro…
Deadlock-Free Session Types in Linear Haskell
Wen Kokke, Ornela Dardha
Priority Sesh is a library for session-typed communication in Linear Haskell which offers strong compile-time correctness guarantees. Priority Sesh offers two deadlock-free APIs fo…
Row-Polymorphic Types for Strategic Rewriting
Rongxiao Fu, Xueying Qin, Ornela Dardha +1
We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to…
Prioritise the Best Variation
Wen Kokke, Ornela Dardha
Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical…
Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics
Ornela Dardha, Jurriaan Rot
This volume contains the proceedings of EXPRESS/SOS 2020: the Combined 27th International Workshop on Expressiveness in Concurrency and the 17th Workshop on Structural Operational…
π with leftovers: a mechanisation in Agda
Uma Zalakain, Ornela Dardha
Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across su…
Comparing Type Systems for Deadlock Freedom
Ornela Dardha, Jorge A. Pérez
Message-passing software systems exhibit non-trivial forms of concurrency and distribution; they are expected to follow intended protocols among communicating services, but also to…
Comparing Deadlock-Free Session Typed Processes
Ornela Dardha, Jorge A. Pérez
Besides respecting prescribed protocols, communication-centric systems should never "get stuck". This requirement has been expressed by liveness properties such as progress or (dea…
Recursive Session Types Revisited
Ornela Dardha
Session types model structured communication-based programming. In particular, binary session types for the pi-calculus describe communication between exactly two participants in a…