@inproceedings{a1d45db5c87a4e298c2c26f54474a11f,
title = "Formal verification of data type refinement theory and practice",
abstract = "This paper develops two theories of data abstraction and refinement: one for applicative types, as they are found in functional programming languages, and one for state-based types found in imperative languages. The former are modelled by algebraic structures, the latter by automata. The automaton-theoretic model covers not just data types but distributed systems in general. Within each theory two examples of data refinement are presented and formally verified with the theorem prover Isabelle. The examples are an abstract specification and two implementations of a memory system, and a mutual exclusion algorithm.",
keywords = "Abstract Data Types, Data Types, Distributed Processes, Implementation, Refinement, Theorem Proving, Verification",
author = "Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1990.; REX Workshop on Stepwise Refinement of Distributed Systems, 1989 ; Conference date: 29-05-1989 Through 02-06-1989",
year = "1990",
doi = "10.1007/3-540-52559-9_79",
language = "English",
isbn = "9783540525592",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "561--591",
editor = "{de Bakker}, J.W. and {de Roever}, W.-P. and G. Rozenberg",
booktitle = "Stepwise Refinement of Distributed Systems",
}