顺序核心Erlang的帧堆栈语义
摘要：使用Coq证明助手,我们提出了顺序Core Erlang的小步骤、帧堆栈样式的语义。该语言是一种动态类型、不纯净的函数式编程语言。我们通过包括异常和异常处理、内置数据类型和函数等改进了之前的工作。基于这个语义，我们定义了多个程序等价的概念(上下文、CIU等价和基于逻辑关系的等价)并证明了这些定义都是等价的。利用这一点，我们能够通过上下文等价的符号表达式对来给出重构的正确性标准，这是本工作的主要动机之一。
作者：P''eter Bereczky, D''aniel Horp''acsi, Simon Thompson
论文ID：2308.12403
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-25