publications
publications by categories in reversed chronological order.
2023
- PLACES’23Kind Inference for the FreeST Programming LanguageBernardo Almeida, Andreia Mordido, and Vasco T. VasconcelosIn PLACES@ETAPS, Paris, France 2023
We present a kind inference algorithm for the FREEST programming language. The input to the algorithm is FREEST source code with (possibly part of) kind annotations replaced by kind variables. The algorithm infers concrete kinds for all kind variables. We ran the algorithm on the FREEST test suite by first replacing kind annotation on all type variables by fresh kind variables, and concluded that the algorithm correctly infers all kinds. Non surprisingly, we found out that programmers do not choose the most general kind in 20% of the cases.
@inproceedings{DBLP:journals/corr/abs-2304-06396, url_custom = {https://doi.org/10.4204/EPTCS.378.1}, author = {Almeida, Bernardo and Mordido, Andreia and Vasconcelos, Vasco T.}, editor = {Castellani, Ilaria and Scalas, Alceste}, title = {Kind Inference for the FreeST Programming Language}, booktitle = {PLACES@ETAPS, Paris, France}, series = {{EPTCS}}, volume = {378}, pages = {1--13}, year = {2023}, url = {https://doi.org/10.4204/EPTCS.378.1}, doi = {10.4204/EPTCS.378.1}, timestamp = {Mon, 05 Feb 2024 20:19:03 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2304-06396.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
2022
- Inf. & Comp.Polymorphic lambda calculus with context-free session typesInformation and Computation 2022
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.
@article{ALMEIDA2022104948, url_custom = {https://www.sciencedirect.com/science/article/pii/S0890540122001031}, title = {Polymorphic lambda calculus with context-free session types}, journal = {Information and Computation}, pages = {104948}, year = {2022}, issn = {0890-5401}, doi = {https://doi.org/10.1016/j.ic.2022.104948}, url = {https://www.sciencedirect.com/science/article/pii/S0890540122001031}, author = {Almeida, Bernardo and Mordido, Andreia and Thiemann, Peter and Vasconcelos, Vasco T.}, keywords = {Polymorphism, Functional programming, Session types, Context-free types} } - Doct. Symp.’22Context-free Session Types: Theory and PracticeBernardo AlmeidaDoctoral Symposium@ECOOP 2022
Communication plays a significant role in concurrent software systems. The concurrent agents that communicate with each other may exchange a massive number of messages and, to avoid unexpected behaviours, these messages should follow a protocol capable of accounting for their order and form. Session types offer mechanisms to model these interactions while ensuring safety properties like the absence of communication errors and deadlocks. They describe structured interaction of processes on heterogeneously typed communication channels. Regular session types impose that protocols must have a tail-recursive structure. On the other hand, context-free session types, proposed by Thiemann and Vasconcelos, drop the tail recursion restriction, thus allowing recursion to occur at any part of the type. The resulting system bears enhanced session types, capable of defining protocols that describe the serialisation of non-regular structures. Moreover, context-free session types can define complex protocols like serialising a tree-like structure without resorting to techniques like higher-order channels. Our work is based on FreeST, a concurrent programming language based on a core functional language, with primitives for creating new threads, new channels and communicating on those channels. In FreeST, channels are bidirectional and governed by context-free session types. With this work, we aim to increase the usability of FreeST by introducing impredicative polymorphism, by adding higher-order kinds and type operators, and by adopting algorithms that provide local type inference.
@article{AlmeidaDS22, title = {Context-free Session Types: Theory and Practice}, journal = {Doctoral Symposium@ECOOP}, year = {2022}, author = {Almeida, Bernardo} } - INFORUM’22Sharing the Stateful WorldIn INFORUM@Guarda, Portugal 2022
Writing concurrent programs with races is cumbersome and may dictate the fall of any software. The difficulty in writing concurrent programs often originates from complex communication patterns among different parties. FreeST was born with the purpose of simplifying the specification and implementation of communicating systems through the use of session types, supported by a powerful type checker. Unfortunately, linear session types are bound to a 1-to-1 communication which means that cooperation between more than two processes is neither simple nor efficient. In this work, we propose shared context-free session types to overcome this restriction. This newly implemented feature opens up a new world of use cases, which include shared state, producer-consumer architectures, and FreeST’s standard IO. This paper uses a store as a running example to show how shared channels improve FreeST’s usability in comparison to linear channels, and how it maintains expressiveness without complicating code.
@inproceedings{inforum22, author = {Barros, Diogo and Mordido, Andreia and Vasconcelos, Vasco T. and Almeida, Bernardo}, editor = {Freire, M{\'a}rio and Pato, Matilde}, title = {Sharing the Stateful World}, booktitle = {INFORUM@Guarda, Portugal}, pages = {27--38}, year = {2022} }
2020
- TACAS’20Deciding the Bisimilarity of Context-Free Session TypesBernardo Almeida, Andreia Mordido, and Vasco T. VasconcelosIn TACAS, Held as Part of ETAPS 2020
We present an algorithm to decide the equivalence of context-free session types, practical to the point of being incorporated in a compiler. We prove its soundness and completeness. We further evaluate its behaviour in practice. In the process, we introduce an algorithm to decide the bisimilarity of simple grammars.
@inproceedings{DBLP:conf/tacas/AlmeidaMV20, url_custom = {https://doi.org/10.1007/978-3-030-45237-7\_3}, author = {Almeida, Bernardo and Mordido, Andreia and Vasconcelos, Vasco T.}, editor = {Biere, Armin and Parker, David}, title = {Deciding the Bisimilarity of Context-Free Session Types}, booktitle = {{TACAS}, Held as Part of {ETAPS}}, series = {LNCS}, volume = {12079}, pages = {39--56}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-45237-7\_3}, doi = {10.1007/978-3-030-45237-7\_3}, timestamp = {Mon, 04 May 2020 13:23:20 +0200}, biburl = {https://dblp.org/rec/conf/tacas/AlmeidaMV20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } - ESOP’20Mixed SessionsIn ESOP, Held as Part of ETAPS 2020
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 picks exactly one. This sort of choice constitutes a particular case of separated choice: offering on one side, selecting on the other. 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 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. Finally, we discuss algorithmic type checking and a runtime system built on top of a conventional (choice-less) message-passing architecture.
@inproceedings{DBLP:conf/esop/VasconcelosCAM20, url_custom = {https://doi.org/10.1007/978-3-030-44914-8\_26}, author = {Vasconcelos, Vasco T. and Casal, Filipe and Almeida, Bernardo and Mordido, Andreia}, editor = {M{\"{u}}ller, Peter}, title = {Mixed Sessions}, booktitle = {{ESOP}, Held as Part of {ETAPS}}, series = {LNCS}, volume = {12075}, pages = {715--742}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-44914-8\_26}, doi = {10.1007/978-3-030-44914-8\_26}, timestamp = {Mon, 04 May 2020 13:23:23 +0200}, biburl = {https://dblp.org/rec/conf/esop/VasconcelosCAM20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
2019
- PLACES’19FreeST: Context-free Session Types in a Functional LanguageBernardo Almeida, Andreia Mordido, and Vasco T. VasconcelosIn PLACES@ETAPS, Prague, Czech Republic 2019
FreeST is an experimental concurrent programming language. Based on a core linear functional programming language, it features primitives to fork new threads, and for channel creation and communication. A powerful type system of context-free session types governs the interaction on channels. The compiler builds on a novel algorithm for deciding type equivalence of context-free session types. This abstract provides a gentle introduction to the language and discusses the validation process and runtime system.
@inproceedings{DBLP:journals/corr/abs-1904-01284, url_custom = {https://doi.org/10.4204/EPTCS.291.2}, author = {Almeida, Bernardo and Mordido, Andreia and Vasconcelos, Vasco T.}, editor = {Martins, Francisco and Orchard, Dominic}, title = {FreeST: Context-free Session Types in a Functional Language}, booktitle = {PLACES@ETAPS, Prague, Czech Republic}, series = {{EPTCS}}, volume = {291}, pages = {12--23}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.291.2}, doi = {10.4204/EPTCS.291.2}, timestamp = {Sat, 19 Oct 2019 19:22:56 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1904-01284.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } - INFORUM’22Uma linguagem de programação com escolhas mistas em tipos de sessãoBernardo Almeida, Andreia Mordido, and Vasco T. VasconcelosIn Atas do 11º Simpósio de Informática 2019
A abstração e formalização da comunicação inerente a sistemas de software é fundamental para a confiabilidade de sistemas concorrentes. Neste trabalho propomos um sistema de tipos que enriquece os tipos de sessão, permitindo escolhas mistas entre input e output. Na linguagem que propomos, FreestMC, os processos podem, a cada momento, decidir entre ler e escrever num dado canal. Um sistema de tipos de sessão garante, ainda assim, que os processos seguem o protocolo.
@inproceedings{inforum19, author = {Almeida, Bernardo and Mordido, Andreia and Vasconcelos, Vasco T.}, title = {Uma linguagem de programa{\c{c}}{\~a}o com escolhas mistas em tipos de sess{\~a}o}, year = {2019}, booktitle = {Atas do 11º Simp{\'o}sio de Inform{\'a}tica} }
2018
- INFORUM’18Uma linguagem de programação com tipos de sessão independentes do contextoBernardo Almeida, and Vasco T. VasconcelosIn Atas do 10º Simpósio de Informática 2018
Os sistemas de software distribuídos têm uma comunicação bastante intensiva onde o elevado número de mensagens trocadas entre processos tende a tornar a codificação dos mesmos bastante complexa. Os tipos de sessão foram propostos para responder a esta necessidade, permitindo definir protocolos na forma de tipos que representam "interações corretas" do sistema e que garantem propriedades tais como a inexistência de erros na comunicação e de situações de impasse. Os tipos de sessão tradicionais são descritos por linguagens regulares, permitindo, por exemplo, a definição de protocolos na forma de lista mas não em forma de árvore. Neste artigo apresenta-se uma linguagem de programação concorrente, explicitamente tipificada, onde os processos comunicam exclusivamente por troca de mensagens cujos protocolos são definidos por tipos de sessão livres do contexto.
@inproceedings{inforum18, author = {Almeida, Bernardo and Vasconcelos, Vasco T.}, title = {Uma linguagem de programa{\c{c}}{\~a}o com tipos de sess{\~a}o independentes do contexto}, booktitle = {Atas do 10º Simp{\'o}sio de Inform{\'a}tica}, year = {2018} } - M.Sc. ThesisAlmeida, B. (2018). Uma linguagem de programação com tipos de sessão independentes do contexto.
@thesis{almeida2018linguagem, url_custom = {https://repositorio.ul.pt/handle/10451/36701}, title = {Uma linguagem de programa{\c{c}}{\~a}o com tipos de sess{\~a}o independentes do contexto}, author = {Almeida, Bernardo}, year = {2018} }