author kleing
Fri, 27 Oct 2000 15:11:49 +0200
changeset 10345 487acfd5f2d2
parent 10180 149878bae19c
child 10462 adf901eb9c40
permissions -rw-r--r--
removed isabelle resources: are available from main pages

Isabelle at Munich


<h1>Isabelle at Munich</h1> 


<a href="">Isabelle</a> is a generic theorem
proving environment developed at Cambridge University (<a
href="">Larry Paulson</a>) and TU
Munich (<a href="">Tobias Nipkow</a>).
This is the local page of the Munich group.


The following people are involved in Isabelle applications or
development at our group (alphabetical order):


<li> <a href="">Gertrud Bauer</a>
<li> <a href="">Stefan Berghofer</a>
<li> <a href="">Gerwin Klein</a>
<li> <a href="">Wolfgang Naraschewski</a>
<li> <a href="">Tobias Nipkow</a>
<li> <a href="">David von Oheimb</a>
<li> <a href="">Leonor Prensa Nieto</a>
<li> <a href="">Cornelia Pusch</a>
<li> <a href="">Markus Wenzel</a>



The main Isabelle related projects at TU Munich are currently:


<li> <b><a href="Bali/index.html">Isabelle/Bali</a></b> Java and JVM
formalization --- type system, semantics, compilers

<li> <b><a href="Isar/index.html">Isabelle/Isar</a></b> Intelligible
semi-automated reasoning --- readable formal proof documents

<li><b><a href="IOA/index.html">Isabelle/IOA</a></b> Verification of
distributed, reactive systems using I/O Automata

<li> <b>Isabelle/HOOL</b> Object-oriented verification of
object-oriented programs



<b>Important local information:</b> Students are welcome to
participate, see <a href="stud/index.html">Isabelle Projekte für
Studenten</a> (in German) for more information.