Restricting destructive update to values of a distinguished reference type prevents functions from being polymorphic in the mutability of their arguments. This restriction makes it easier to reason about program behaviour during transformation, but the lack of polymorphism reduces the expressiveness of the language. We present a System-F style core language that uses dependently kinded proof witnesses to encode information about the mutability of values and the purity of computations. We support mixed strict and lazy evaluation, and use our type system to ensure that only computations without visible side effects are suspended. © 2009 Springer-Verlag.
CITATION STYLE
Lippmeier, B. (2009). Witnessing purity, constancy and mutability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5904 LNCS, pp. 95–110). https://doi.org/10.1007/978-3-642-10672-9_9
Mendeley helps you to discover research relevant for your work.