Refinement types in Jolie

TL;DR

This paper explores integrating refinement types into Jolie, a microservices language, to combine static and dynamic type checking for improved security and reduced testing effort using SMT solvers.

Contribution

It introduces the concept of refinement types in Jolie and demonstrates how they enable combined static and dynamic verification for microservices.

Findings

Refinement types can be integrated into Jolie for enhanced type safety.

Static verification of internal services is complemented by dynamic checks for external services.

The approach improves security and reduces testing effort.

Abstract

Jolie is the first language for microservices and it is currently dynamically type checked. This paper considers the opportunity to integrate dynamic and static type checking with the introduction of refinement types, verified via SMT solver. The integration of the two aspects allows a scenario where the static verification of internal services and the dynamic verification of (potentially malicious) external services cooperates in order to reduce testing effort and enhancing security.