Actor programming is a concurrency model where independent entities called “actors” communicate by passing messages and are found in languages such as Erlang and Elixir. Multiparty session types specify communication protocols among multiple participants, ensuring that all follow a shared protocol and ruling out errors like deadlocks or message mismatches at compile time. Maty is the first actor language design supporting both static multiparty session typing and the full power of actors taking part in multiple sessions.

The Goal of this lab is to reproduce and/or formalize a project in the distributed programming realm, for example Maty, using the programming language Lean.