src/HOLCF/IOA/README.html
changeset 5843 136a51f95c91
parent 5138 b02dfb930bd9
child 5844 2886310fb5e9
     1.1 --- a/src/HOLCF/IOA/README.html	Mon Nov 09 15:50:56 1998 +0100
     1.2 +++ b/src/HOLCF/IOA/README.html	Tue Nov 10 16:27:04 1998 +0100
     1.3 @@ -5,30 +5,11 @@
     1.4  Author:     Olaf M&uuml;ller<BR>
     1.5  Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
     1.6  
     1.7 -The distribution contains:
     1.8 -<UL>
     1.9 -  <li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion
    1.10 -       and the compositionality of the model. For details see: <BR>
    1.11 -       Olaf M&uuml;ller and Tobias Nipkow,
    1.12 -       <A HREF="http://www4.informatik.tu-muenchen.de/papers/tapsoft_mueller_1997_Conference.html">Traces of I/O Automata in Isabelle/HOLCF</A>.
    1.13 -In <i> TAPSOFT'97, Proc. of the 7th  International Joint Conference on Theory and Practice of Software Development </i>, LNCS 1224, 1997.<P>
    1.14 -
    1.15 -  <li> A proof of the Alternating Bit Protocol (ABP subdirectory) with unbounded buffers using 
    1.16 -       a combination of Isabelle and a model checker. This case study is performed within the 
    1.17 -       theory of IOA described above. For details see:<BR>
    1.18 -Olaf M&uuml;ller and Tobias Nipkow,
    1.19 -<A HREF="http://www4.informatik.tu-muenchen.de/papers/MuellerNipkow_TaAf1995.html">Combining Model Checking and Deduction for I/O Automata  </A>.
    1.20 -In <i> TACAS'95, Proc. of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems </i>, LNCS 1019, 1995.<P>
    1.21 -   <li> A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:<BR>
    1.22 -
    1.23 -        Tobias Nipkow, Konrad Slind.
    1.24 -<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/types94.html>
    1.25 -I/O Automata in Isabelle/HOL</A>. In <i>Types for Proofs and Programs</i>,
    1.26 -LNCS 996, 1995, 101-119.
    1.27 -
    1.28 -</UL>
    1.29 +The distribution contains simulation relations, temporal logic, and an abstraction theory.
    1.30 +Everything is based upon a domain-theoretic model of finite and infinite sequences. 
    1.31 +<p>
    1.32 +For details see <A HREF="http://www4.informatik.tu-muenchen.de/~isabelle/IOA/">IOA project</a>.
    1.33  
    1.34  </BODY></HTML>
    1.35  
    1.36  
    1.37 -