Sciweavers

Share
POPL
2008
ACM

Lightweight semiformal time complexity analysis for purely functional data structures

9 years 2 months ago
Lightweight semiformal time complexity analysis for purely functional data structures
Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees. Categories and Subject Descriptors F.2.m [Analysis of Algorithms and Problem Complexity]: Miscellaneous; F.3.1 [Logics and Meanings of Programs]: Specifying an...
Nils Anders Danielsson
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where POPL
Authors Nils Anders Danielsson
Comments (0)
books