Author name cluster

Vasco T. Vasconcelos

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

TCS Journal 2026 Journal Article

Subtyping context-free session types

Gil Silva
Andreia Mordido
Vasco T. Vasconcelos

Session types are a type discipline for concurrent programming. They allow programmers to describe and enforce structured patterns of communication between processes on heterogeneous, bidirectional channels. Equipped with a sequential composition operator, context-free session types enjoy greater expressive power when compared to their traditional counterparts, which are limited to the specification of regular communication patterns. The introduction of subtyping allows programmers to draw on this enhanced expressive power to describe even richer behaviors while avoiding code duplication. In this work, we present the first dedicated study of subtyping for context-free session types, which has until now been only briefly considered and, somewhat discouragingly, found undecidable. Despite this unfortunate result, we define a rich notion of subtyping for context-free session types in a functional setting, and present two distint approaches to its formalization: one based on inference rules, the other based on a labelled transition system. For the latter, we introduce XYZW -simulations, a novel family of simulation relations that generalize both XY -simulations and polar simulations. We further propose a semi-algorithm for the problem, prove it to be sound, and evaluate it empirically in the context of a programming language compiler.

Details DOI

TCS Journal 2024 Journal Article

Polymorphic higher-order context-free session types

Diana Costa
Andreia Mordido
Diogo Poças
Vasco T. Vasconcelos

We present an extension of polymorphic context-free session types that allows passing channels on channels, commonly known as higher-order session types. The mixture of functional types and session types has proven to be a challenge for type equivalence formulation: whereas functional type equivalence is often inductive and presented as a system of derivation rules, session type equivalence is often coinductive and usually presented as a bisimulation. We propose a unifying approach that handles the equivalence of functional and higher-order context-free session types together in the form of a system of rules generating a coinductively defined relation. Decidability of type equivalence is obtained via reduction to bisimulation for simple grammars, for which practical algorithms are known. To bridge the gap between types and simple grammars, we introduce a language of types with canonical names instead of bindings (which we call c-types), and propose a notion of canonical renaming to translate types to c-types.

Details DOI

TCS Journal 2022 Journal Article

Mixed sessions

Filipe Casal
Andreia Mordido
Vasco T. Vasconcelos

Session types describe patterns of interaction on communicating channels. Traditional session types include a form of choice whereby servers offer a collection of options, of which each client selects exactly one. Mixed choices blur the distinction between servers and clients (that is, external and internal choice) by allowing options to be both offered and selected in the same choice. We introduce mixed choices in the context of session types and argue that they increase the flexibility of program development at the same time that they reduce the number of synchronisation primitives down to exactly one. We present a type system incorporating subtyping and prove preservation and absence of runtime errors for well-typed processes. We further show that classical (conventional) sessions can be faithfully and tightly embedded in mixed choices, and conversely that there is a minimal encoding from mixed choices to classical sessions. Finally, we discuss algorithmic type checking and a runtime system built on top of a conventional (choice-less) message-passing architecture.

Details DOI

I&C Journal 2022 Journal Article

Polymorphic lambda calculus with context-free session types

Bernardo Almeida
Andreia Mordido
Peter Thiemann
Vasco T. Vasconcelos

Session types provide a typing discipline for structured communication on bidirectional channels. Context-free session types overcome the restriction to tail recursive protocols characteristic of conventional session types. This extension enables the serialization and deserialization of tree structures in a fully type-safe manner. We present the theory underlying the language FreeST 2, which features context-free session types in an extension of System F with linear types and a kinding system to distinguish message types, session types, and channel types. The system presents metatheoretical challenges which we address: contractivity in the presence of polymorphism, a non-trivial equational theory on types, and decidability of type equivalence. We also establish standard results on typing preservation, progress, and a characterization of erroneous processes.

Details DOI

I&C Journal 2012 Journal Article

An Algebra of Behavioural Types

António Ravara
Pedro Resende
Vasco T. Vasconcelos

We propose a process algebra, the Algebra of Behavioural Types, as a language for typing concurrent objects. A type is a higher-order labelled transition system that characterises all possible life cycles of a concurrent object. States represent interfaces of objects; state transitions model the dynamic change of object interfaces. Moreover, a type provides an internal view of the objects that inhabits it: a synchronous one, since transitions correspond to message reception. To capture this internal view of objects we define a notion of bisimulation, strong on labels and weak on silent actions. We study several algebraic laws that characterise this equivalence, and obtain completeness results for image-finite types.

Details DOI

I&C Journal 2012 Journal Article

Fundamentals of session types

Vasco T. Vasconcelos

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; unrestricted (or shared) channels may appear in an unbounded number of threads. In our language each channel is characterized 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 the same channel. This mechanism allows a precise control of resources via a conventional linear type system. Furthermore, the uniform treatment of linear and shared channels leads to a surprisingly simply theory which, in addition, extends typability when compared to traditional systems for session types. We build the language gradually, starting from simple input/output, then adding recursive types, replication and finally choice. We also present an algorithmic type checking system.

Details DOI

TCS Journal 2006 Journal Article

Type checking a multithreaded functional language with session types

Vasco T. Vasconcelos
Simon J. Gay
António Ravara

We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static type checking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus type checking can verify both correctness of individual messages and correctness of sequences of transitions. Previously, session types have mainly been studied in the context of the π -calculus; instead, our formulation is based on a multithreaded functional language with side-effecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and type checking system of our language, and prove subject reduction and runtime type safety theorems.

Details DOI