FreeST is a typed concurrent programming language where processes communicate via message-passing.

Messages are exchanged on bidirectional channels. Communication on channels is governed by a powerful type system based on polymorphic context-free session types. Based on a core linear functional programming language, FreeST features primitives for forking new threads and for creating, and communicating on, channels. The compiler builds on a novel algorithm for deciding the equivalence of context-free session types (short tutorial).



FreeST – Try FreeST on your browser.

CFSTEquiv – A tool that tests whether two context-free session types are equivalent.

SGBisim – A tool that checks whether two non-terminal symbols in simple grammar are bisimilar.


Publications, talks, posters

Almeida, B., Mordido A. and Vasconcelos V.T., 2020. Deciding the Bisimilarity of Context-free Session Types. In TACAS 2020, LNCS, vol 12079, pp. 39-56. Springer.

Session Type Equivalence via Bisimulation, talk at Carnegie Mellon University, 2019.

Almeida, B., Mordido, A. and Vasconcelos, V.T., 2019. FreeST: Context-free Session Types in a Functional Language, In PLACES 2019, EPTCS, vol 291, pp. 12-23.

FreeST: Context-free Session Types in a Concurrent Functional Language, talk at Programming Languages for Distributed Systems, Shonan, 2019.

FreeST: Context-free Session Types in a Functional Language, poster at ETAPS 2019.

Thiemann, P. and Vasconcelos, V.T., 2016. Context-free Session Types. In ICFP 2016, ACM, pp. 462-475.