isabelle: src/HOLCF/IOA/README.html@2bd87b6682bf (annotated)

3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	1	<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	2
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	3	<H3>IOA: A formalization of I/O automata in HOLCF</H3>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	4
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	5	Author: Olaf Mueller<BR>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	6	Copyright 1997 Technische Universität München<P>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	7
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	8	Version: 1.0<BR>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	9	Date: 1.05.97<P>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	10
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	11	The distribution contains
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	12
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	13	<UL>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	14	<li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	15	and the compositionality of the model. For details see: <BR>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	16	Olaf Müller and Tobias Nipkow,
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	17	<A HREF="http://www4.informatik.tu-muenchen.de/papers/tapsoft_mueller_1997_Conference.html">Traces of I/O Automata in Isabelle/HOLCF</A>.
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	18	In <i> TAPSOFT'97, Proc. of the 7th International Joint Conference on Theory and Practice of Software Development </i>, LNCS 1224, 1997.<P>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	19
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	20	<li> A proof of the Alternating Bit Protocol (ABP subdirectory) with unbounded buffers using
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	21	a combination of Isabelle and a model checker. This case study is performed within the
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	22	theory of IOA described above. For details see:<BR>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	23	Olaf Müller and Tobias Nipkow,
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	24	<A HREF="http://www4.informatik.tu-muenchen.de/papers/MuellerNipkow_TaAf1995.html">Combining Model Checking and Deduction for I/O Automata </A>.
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	25	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>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	26	<li> A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:<BR>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	27
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	28	Tobias Nipkow, Konrad Slind.
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	29	<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ioa.html>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	30	I/O Automata in Isabelle/HOL</A>. In <i>Types for Proofs and Programs</i>,
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	31	LNCS 996, 1995, 101-119.
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	32
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	33	</UL>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	34
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	35	</BODY></HTML>
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	36
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	37
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	38

author	wenzelm
	Mon, 12 May 1997 14:58:45 +0200
changeset 3158	2bd87b6682bf
parent 3071	981258186b71
child 3279	815ef5848324
permissions	-rw-r--r--