Bernardo Almeida

Dept. of Informatics - 6.3.29

Campo Grande, 1749-016

Lisboa, Portugal

I am a PhD student at the Faculty of Sciences of the University of Lisbon. Currently, I am working at the LASIGE research unit.

My main research topics are programming languages, type systems, and session types. I am interested in type systems in general, but I am mainly focused on session types. Session types allow describing structured communication patterns, and they really shine in the presence of concurrency. Furthermore, through these sophisticated type systems, one can guarantee, at compile time, the absence of communication errors. Therefore, I consider that capturing bad communication behaviours is essential to all concurrent programming languages.

Currently, I am the lead developer of FreeST, a functional concurrent programming language where processes communicate via message-passing. The language features bi-directional channel-based communication. In FreeST, all communication is governed by context-free session types.

news

Aug 5, 2022	Our article “Polymorphic lambda calculus with context-free session types”, has been accepted at Information and Computation.

selected publications

PLACES’23

Kind Inference for the FreeST Programming Language

Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos

In PLACES@ETAPS, Paris, France 2023

Abs Bib URL

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}
}

Inf. & Comp.
Polymorphic lambda calculus with context-free session types

Bernardo Almeida, Andreia Mordido, Peter Thiemann, and 1 more author

Information and Computation 2022

Abs Bib URL

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} }

TACAS’20

Deciding the Bisimilarity of Context-Free Session Types

Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos

In TACAS, Held as Part of ETAPS 2020

Abs Bib URL

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’20
Mixed Sessions

Vasco T. Vasconcelos, Filipe Casal, Bernardo Almeida, and 1 more author

In ESOP, Held as Part of ETAPS 2020

Abs Bib URL

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} }