Admin/page/main-content/munich.content

eliminated theories "equalities" and "mono" (made part of "Typedef",
which supercedes "subset");

+
−%title%
+
−Isabelle at Munich
+
−
+
−
+
−%body%
+
−
+
−<h1>Isabelle at Munich</h1> 
+
−
+
−<p>
+
−
+
−<a href="http://isabelle.in.tum.de/">Isabelle</a> is a generic theorem
+
−proving environment developed at Cambridge University (<a
+
−href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
+
−Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
+
−This is the local page of the Munich group.
+
−
+
−
+
−<h2>People</h2>
+
−
+
−The following people are involved in Isabelle applications or
+
−development in our group (alphabetical order):
+
−<p>
+
−<b>Researches:</b>
+
−
+
−<ul>
+
−
+
−<li><a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a>
+
−<li><a href="http://www4.in.tum.de/~berghofe/">Stefan Berghofer</a>
+
−<li><a href="http://www4.in.tum.de/~kleing/">Gerwin Klein</a>
+
−<li><a href="http://www4.in.tum.de/~narasche/">Wolfgang Naraschewski</a>
+
−<li><a href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a>
+
−<li><a href="http://www4.in.tum.de/~oheimb/">David von Oheimb</a>
+
−<li><a href="http://www4.in.tum.de/~prensani/">Leonor Prensa Nieto</a>
+
−<li><a href="http://www4.in.tum.de/~pusch/">Cornelia Pusch</a>
+
−<li><a href="http://www4.in.tum.de/~streckem/">Martin Strecker</a>
+
−<li><a href="http://www4.in.tum.de/~wenzelm/">Markus Wenzel</a>
+
−
+
−</ul>
+
−
+
−<p>
+
−<b>Students:</b>
+
−
+
−<ul>
+
−
+
−<li><a href="mailto:[e-mail]">Christian Buttenberg</a> </li>
+
−<li><a href="http://home.informatik.tu-muenchen.de/~kirsch/">Alexandra Kirsch</a> </li>
+
−<li><a href="http://www.informatik.tu-muenchen.de/~nanz/">Sebastian Nanz</a> </li>
+
−<li><a href="http://www.informatik.tu-muenchen.de/~pfeifrot/">Johannes Pfeifroth</a> </li>
+
−
+
−</ul>
+
−
+
−
+
−<h2>Projects</h2>
+
−
+
−The main Isabelle related projects at TU Munich are currently:
+
−
+
−<ul>
+
−
+
−<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
+
−
+
−<li><b><a href="VerifiCard/">Isabelle/VerifiCard</a></b> Tool-assisted
+
−Specification and Verification of JavaCard� Programs
+
−
+
−</ul>
+
−
+
−<p>
+
−
+
−<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.