src/HOLCF/IOA/README.html
changeset 3071 981258186b71
child 3279 815ef5848324
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/README.html	Wed Apr 30 11:20:15 1997 +0200
     1.3 @@ -0,0 +1,38 @@
     1.4 +<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
     1.5 +
     1.6 +<H3>IOA: A formalization of I/O automata in HOLCF</H3>
     1.7 +
     1.8 +Author:     Olaf Mueller<BR>
     1.9 +Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
    1.10 +
    1.11 +Version: 1.0<BR>
    1.12 +Date: 1.05.97<P>
    1.13 +
    1.14 +The distribution contains
    1.15 +
    1.16 +<UL>
    1.17 +  <li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion
    1.18 +       and the compositionality of the model. For details see: <BR>
    1.19 +       Olaf M&uuml;ller and Tobias Nipkow,
    1.20 +       <A HREF="http://www4.informatik.tu-muenchen.de/papers/tapsoft_mueller_1997_Conference.html">Traces of I/O Automata in Isabelle/HOLCF</A>.
    1.21 +In <i> TAPSOFT'97, Proc. of the 7th  International Joint Conference on Theory and Practice of Software Development </i>, LNCS 1224, 1997.<P>
    1.22 +
    1.23 +  <li> A proof of the Alternating Bit Protocol (ABP subdirectory) with unbounded buffers using 
    1.24 +       a combination of Isabelle and a model checker. This case study is performed within the 
    1.25 +       theory of IOA described above. For details see:<BR>
    1.26 +Olaf M&uuml;ller and Tobias Nipkow,
    1.27 +<A HREF="http://www4.informatik.tu-muenchen.de/papers/MuellerNipkow_TaAf1995.html">Combining Model Checking and Deduction for I/O Automata  </A>.
    1.28 +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.29 +   <li> A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:<BR>
    1.30 +
    1.31 +        Tobias Nipkow, Konrad Slind.
    1.32 +<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ioa.html>
    1.33 +I/O Automata in Isabelle/HOL</A>. In <i>Types for Proofs and Programs</i>,
    1.34 +LNCS 996, 1995, 101-119.
    1.35 +
    1.36 +</UL>
    1.37 +
    1.38 +</BODY></HTML>
    1.39 +
    1.40 +
    1.41 +