Lucretia - a type system for objects in languages with reflection

TL;DR

Lucretia is a type system designed for object-oriented scripting languages with reflection, enabling automatic control of object structures to improve program stability, with proven soundness and subject reduction.

Contribution

It introduces Lucretia, a novel type system for reflective languages, ensuring object structure control and formal soundness proofs.

Findings

Proves subject reduction for Lucretia

Establishes soundness of the type system

Enables automatic object property control

Abstract

Object-oriented scripting languages such as JavaScript or Python gain in popularity due to their flexibility. Still, the growing code bases written in the languages call for methods that make possible to automatically control the properties of the programs that ensure their stability in the running time. We propose a type system, called Lucretia, that makes possible to control the object structure of languages with reflection. Subject reduction and soundness of the type system with respect to the semantics of the language is proved.