Traces of I/O-Automata in Isabelle/HOLCF

Abstract. This paper presents a formalization of nite and in nite 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 re nement 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 re nement concept in I/O automata.

• Type: Conference
• Year: 1997
• Where: TAPSOFT
• Authors: Olaf Müller, Tobias Nipkow
• Keywords: Domain Theory, I/O Automata, Software Engineering, TAPSOFT 1997, Theorem Prover Isabelle