Traces of I/O-Automata in Isabelle/HOLCF

13 years 8 months ago
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.
Olaf Müller, Tobias Nipkow
Added 08 Aug 2010
Updated 08 Aug 2010
Type Conference
Year 1997
Authors Olaf Müller, Tobias Nipkow
Comments (0)