CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures

Nils Anders Danielsson (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'08; San Francisco, CA; United States; 7 January 2008 through 12 January 2008 (0730-8566). p. 133-144. (2008)
[Konferensbidrag, refereegranskat]

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.



Denna post skapades 2007-11-06. Senast ändrad 2017-12-06.
CPL Pubid: 61165

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)

Ämnesområden

Datalogi

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:


Functional Program Correctness Through Types