Verified type checker for Jolie programming language
This provides a verified type checker for the Jolie programming language, addressing a specific gap in its tooling for developers.
The authors tackled the lack of a tool to ensure well-typed programs in the Jolie language by building a type checker expressed with dependent types in Agda, verifying its correctness as part of a formal model.
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.