Skip navigation
Skip navigation

Witnessing Purity, Constancy and Mutability

Lippmeier, Ben


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...[Show more]

CollectionsANU Research Publications
Date published: 2009
Type: Book chapter
DOI: 10.1007/978-3-642-10672-9_9


File Description SizeFormat Image
01_Lippmeier_Witnessing_Purity,_Constancy_2009.pdf246.42 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator