Lucretia — intersection type polymorphism for scripting languages
Open Access
- 17 March 2015
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 177, 65-78
Abstract
Scripting code may present maintenance problems in the long run. There is, then, the call for methodologies that make it possible to control the properties of programs written in dynamic languages in an automatic fashion. We introduce Lucretia, a core language with an introspection primitive. Lucretia is equipped with a (retrofitted) static type system based on local updates of types that describe the structure of objects being used. In this way, we deal with one of the most dynamic features of scripting languages, that is, the runtime modification of object interfaces. Judgements in our systems have a Hoare-like shape, as they have a precondition and a postcondition part. Preconditions describe static approximations of the interfaces of visible objects before a certain expression has been executed and postconditions describe them after its execution. The field update operation complicates the issue of aliasing in the system. We cope with it by introducing intersection types in method signatures.Comment: In Proceedings ITRS 2014, arXiv:1503.0437Keywords
All Related Versions
This publication has 17 references indexed in Scilit:
- A generic type-and-effect system2009
- Scrap Your Type Applications2008
- An Exploratory Study of How Developers Seek, Relate, and Collect Relevant Information during Software Maintenance TasksIEEE Transactions on Software Engineering, 2006
- Principality and type inference for intersection types using expansion variablesTheoretical Computer Science, 2004
- BabyJElectronic Notes in Theoretical Computer Science, 2003
- Type and Effect Systems1999
- A behavioral notion of subtypingACM Transactions on Programming Languages and Systems, 1994
- Strongtalk1993
- Integrating functional and imperative programming1986
- A filter lambda model and the completeness of type assignmentThe Journal of Symbolic Logic, 1983