@inproceedings{d727fcdc385f4f9f9bc51336d9dca8de,
title = "Traces of i/o-automata in isabelle/HOLCF",
abstract = "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 internM 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.",
author = "Olaf Miiller and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1997.; 7th International Joint Conference on Theory and Practice of Software Development, TAPSOFT 1997 ; Conference date: 14-04-1997 Through 18-04-1997",
year = "1997",
doi = "10.1007/bfb0030627",
language = "English",
isbn = "9783540627814",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "580--594",
editor = "Michel Bidoit and Michel Bidoit and Max Dauchet and Max Dauchet",
booktitle = "TAPSOFT 1997",
}