Verified type-checker for Jolie

Abstract

Jolie is a service-oriented programming language which comes with the formal speci cation 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 ex- press the type checker as a program with dependent types in Agda proof assistant which helps to ascertain that the type checker is correct.