Skip to content
DSML.KZ
Publications

Preprint · arXiv · March 15, 2017

Verified type checker for Jolie programming language

Evgenii Akentev, Alexander Dmitrievich Tchitchigin, Larisa Safina, Manuel Mazzara

Manuel Mazzara
Read on arXivPDFDOI 10.48550/arxiv.1703.05186

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.

Logic, programming, and type systemsService-Oriented Architecture and Web ServicesFormal Methods in Verificationtype checkingdependent typesAgda

More by Manuel Mazzara