Conference item icon

Conference item

Unfolding abstract datatypes

Abstract:
We argue that abstract datatypes - with public interfaces hiding private implementations - represent a form of codata rather than ordinary data, and hence that proof methods for corecursive programs are the appropriate techniques to use for reasoning with them. In particular, we show that the universal properties of unfold operators are perfectly suited for the task. We illustrate with solutions to two problems the solution to a problem in the recent literature. © 2008 Springer-Verlag.
Publication status:
Published

Actions


Access Document


Publisher copy:
10.1007/978-3-540-70594-9_8

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Volume:
5133
Pages:
110-133
Host title:
MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS
Publication date:
2008-01-01
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
Source identifiers:
163474
ISBN:
9783540705932
Pubs id:
pubs:163474
UUID:
uuid:a9f57517-4dea-4055-b627-3aef85f7827c
Local pid:
pubs:163474
Deposit date:
2012-12-19

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP