Bernardo Almeida

selected publications

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

2. TACAS’20

   Deciding the Bisimilarity of Context-Free Session Types

   Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos

   In TACAS 2020, 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} 2020, 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}
   }

3. ESOP’20

   Mixed Sessions

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

   In ESOP 2020, 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} 2020, 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}
   }