Session-Based Typechecking for Elixir Modules Using ElixirST
We investigate the adaptation of session types to provide static behavioural guarantees for Elixir modules. We devise a type system, called ElixirST, which allows us to describe the behaviour of executing a public function in an Elixir module as a protocol of message interactions. The ElixirST type system also allows us to statically determine whether this function observes its endpoint specification; a corresponding tool automating the corresponding typechecking on Elixir source code has also been constructed. We also formally validate this type system. An LTS-based operational semantics for the language fragment supported by the type system is developed, modelling its runtime behaviour when interacting with an arbitrary module client that respects a compatible protocol. This operational semantics is then used to prove a form of session fidelity and progress for ElixirST.
Mon 23 OctDisplayed time zone: Lisbon change
09:00 - 10:30
|Behavioural up/down casting for statically typed languages
|Session-Based Typechecking for Elixir Modules Using ElixirST
|A Semantic Framework for Automatic Composition of Decentralised Industrial Control SchemesCancelled