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.