Publications
Preprint · OSF Preprints · March 2, 2017
Verified type-checker for Jolie
Larisa Safina, Manuel Mazzara, Evgenii Akentev, Alexander Dmitrievich Tchitchigin
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.
Logic, programming, and type systemsService-Oriented Architecture and Web ServicesFormal Methods in Verificationtype checkingdependent typesAgda
More by Manuel Mazzara
- Anchored Rank-Adversarial Fine-Tuning Pretrained Visual Place Recognition ModelsarXiv · 2026
- See the Future, Classify the Present: Stochastic Latent World Modeling for Hyperspectral ImagesarXiv · 2026
- Autoresearch with Coding Agents: Generalizers and Metric-Maximizers on Quran Recitation DataLecture notes in computer science · 2026 · Citations: 1
- What Counts as a Mistake? Annotating Recitation Events in Quran Memorization TranscriptsarXiv · 2026