论文标题
Elixirst的会话保真度：基于会话的类型系统，用于Elixir模块
Session Fidelity for ElixirST: A Session-Based Type System for Elixir Modules
论文作者
论文摘要
本文以先前的工作为基础研究了会话类型的适应，以提供有关长子模块的行为信息。 已经构建了一种称为Elixirst的类型系统，以静态确定Elixir模块中的功能是否观察其端点规格，称为会话类型。还构建了自动化此键入的相应工具。在本文中，我们正式验证了此类型系统。开发了由类型系统支持的语言片段的基于LTS的操作语义，并在模块客户端调用时对其运行时行为进行建模。然后，该操作语义用于证明Elixirst的会话保真度。
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.
