Rytz, LukasAmin, NadaOdersky, Martin2013-05-112013-05-112013-05-11201310.1145/2489804.2489808https://infoscience.epfl.ch/handle/20.500.14299/92058This 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.puritytype-and-effect systemstext::conference output::conference proceedings::conference paper