Skip navigation
Skip navigation

Witnessing Purity, Constancy and Mutability

Lippmeier, Ben

Description

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
URI: http://hdl.handle.net/1885/18993
DOI: 10.1007/978-3-642-10672-9_9

Download

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:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator