Traces of I/O Automata in Isabelle/HOLCF
Olaf Müller and Tobias Nipkow
This paper presents a formalization of finite and infinite sequences
in domain theory carried out in the theorem prover Isabelle. The
results are used to model the metatheory of I/O automata; they are,
however, applicable to any trace based model of parallelism which
distinguishes internal and external actions. We make use of the logic
HOLCF, an extension of HOL with domain theory and show how to move
between HOL and HOLCF. This allows us to restrict the use of HOLCF to
metatheoretic arguments while actual refinement proofs between I/O
automata are carried out within the simpler logic HOL. In order to
evaluate the formalization we prove the correctness of a generalized
refinement concept in I/O automata.
ps
At Springer: http://dx.doi.org/10.1007/BFb0030627
BibTeX:
@inproceedings{Mueller-Nipkow-TAPSOFT-97,
author={Olaf M\"uller and Tobias Nipkow},
title={Traces of {I/O} Automata in {Isabelle/HOLCF}},
booktitle={TAPSOFT'97: Theory and Practice of Software Development},
editor={M. Bidoit and M. Dauchet},
publisher=Springer,series=LNCS,volume=1214,year=1997,pages={580--594},
url={http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tapsoft97.ps.gz}}
The corresponding
Isabelle theories.