Conference icon

Conference

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
Department:
Oxford, MPLS, Computer Science
Volume:
5133
Pages:
110-133
Publication date:
2008
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
URN:
uuid:a9f57517-4dea-4055-b627-3aef85f7827c
Source identifiers:
163474
Local pid:
pubs:163474
ISBN:
978-3-540-70593-2

Terms of use


Metrics



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

TO TOP