A Flow-Insensitive, Modular Effect System for Purity

This article presents a modular, flow-insensitive type-and- effect system for purity with lightweight annotations. It does not enforce a global programming discipline and allows ar- bitrary effects to occur in impure parts of the program. The system is designed to support higher-order languages that mix functional and imperative code, such as Scala or C#. We show that it can express purity of non-local programming patterns which involve mutable state such as those used in the Scala collections library. We formalize the type system using a functional language with mutable records and define a dynamic semantics, a type safety and an effect soundness theorem.


Presented at:
Formal Techniques for Java-like Programs, Montpellier, France, July 1, 2013
Year:
2013
Keywords:
Laboratories:




 Record created 2013-05-11, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)