Jolie 编程语言的经过验证的类型检查器
编程语言
2017-03-24 v2 软件工程
摘要
Jolie 是一种面向服务的编程语言，附带其类型系统的形式化规约。然而，目前没有工具能确保 Jolie 程序是良类型的。在本文中，我们给出了将 Jolie 的类型检查器作为其语法与语义形式模型的一部分进行构建的结果。我们将该类型检查器表示为 Agda 证明助手中的依值类型程序，这有助于确证该类型检查器的正确性。
引用
@article{arxiv.1703.05186,
title = {Verified type checker for Jolie programming language},
author = {Evgenii Akentev and Alexander Tchitchigin and Larisa Safina and Manuel Mazzara},
journal= {arXiv preprint arXiv:1703.05186},
year = {2017}
}