Verified type checker for Jolie programming language
Programming Languages
2017-03-24 v2 Software Engineering
Abstract
Jolie is a service-oriented programming language which comes with the formal specification of its type system. However, there is no tool to ensure that programs in Jolie are well-typed. In this paper we provide the results of building a type checker for Jolie as a part of its syntax and semantics formal model. We express the type checker as a program with dependent types in Agda proof assistant which helps to ascertain that the type checker is correct.
Cite
@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}
}