Session Fidelity for ElixirST: A Session-Based Type System for Elixir Modules

TL;DR

This paper formally validates ElixirST, a session-based type system for Elixir modules, by developing an operational semantics and proving session fidelity to ensure behavioral correctness.

Contribution

It introduces a formal validation of ElixirST, including an operational semantics and proof of session fidelity, advancing static behavioral analysis for Elixir modules.

Findings

Operational semantics models runtime behavior

Session fidelity is formally proven

Type system ensures module compliance with session types

Abstract

This paper builds on prior work investigating the adaptation of session types to provide behavioural information about Elixir modules. A type system called ElixirST has been constructed to statically determine whether functions in an Elixir module observe their endpoint specifications, expressed as session types; a corresponding tool automating this typechecking has also been constructed. In this paper we 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 invoked by the module client. This operational semantics is then used to prove session fidelity for ElixirST.