1 %title% |
|
2 Isabelle at Munich |
|
3 |
|
4 |
|
5 %body% |
|
6 |
|
7 <h1>Isabelle at Munich</h1> |
|
8 |
|
9 <p> |
|
10 |
|
11 <a href="http://isabelle.in.tum.de/">Isabelle</a> is a generic theorem |
|
12 proving environment developed at Cambridge University (<a |
|
13 href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU |
|
14 Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). |
|
15 This is the local page of the Munich group. |
|
16 |
|
17 |
|
18 <h2>People</h2> |
|
19 |
|
20 The following people are involved in Isabelle applications or |
|
21 development in our group (alphabetical order): |
|
22 <p> |
|
23 <b>Researches:</b> |
|
24 |
|
25 <ul> |
|
26 |
|
27 <li><a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a> |
|
28 <li><a href="http://www4.in.tum.de/~berghofe/">Stefan Berghofer</a> |
|
29 <li><a href="http://www4.in.tum.de/~kleing/">Gerwin Klein</a> |
|
30 <li><a href="http://www4.in.tum.de/~narasche/">Wolfgang Naraschewski</a> |
|
31 <li><a href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a> |
|
32 <li><a href="http://www4.in.tum.de/~oheimb/">David von Oheimb</a> |
|
33 <li><a href="http://www4.in.tum.de/~prensani/">Leonor Prensa Nieto</a> |
|
34 <li><a href="http://www4.in.tum.de/~pusch/">Cornelia Pusch</a> |
|
35 <li><a href="http://www4.in.tum.de/~streckem/">Martin Strecker</a> |
|
36 <li><a href="http://www4.in.tum.de/~wenzelm/">Markus Wenzel</a> |
|
37 |
|
38 </ul> |
|
39 |
|
40 <p> |
|
41 <b>Students:</b> |
|
42 |
|
43 <ul> |
|
44 |
|
45 <li><a href="mailto:buttenbe@in.tum.de">Christian Buttenberg</a> </li> |
|
46 <li><a href="http://home.informatik.tu-muenchen.de/~kirsch/">Alexandra Kirsch</a> </li> |
|
47 <li><a href="http://www.informatik.tu-muenchen.de/~nanz/">Sebastian Nanz</a> </li> |
|
48 <li><a href="http://www.informatik.tu-muenchen.de/~pfeifrot/">Johannes Pfeifroth</a> </li> |
|
49 |
|
50 </ul> |
|
51 |
|
52 |
|
53 <h2>Projects</h2> |
|
54 |
|
55 The main Isabelle related projects at TU Munich are currently: |
|
56 |
|
57 <ul> |
|
58 |
|
59 <li><b><a href="Bali/index.html">Isabelle/Bali</a></b> Java and JVM |
|
60 formalization --- type system, semantics, compilers |
|
61 |
|
62 <li><b><a href="Isar/index.html">Isabelle/Isar</a></b> Intelligible |
|
63 semi-automated reasoning --- readable formal proof documents |
|
64 |
|
65 <li><b><a href="IOA/index.html">Isabelle/IOA</a></b> Verification of |
|
66 distributed, reactive systems using I/O Automata |
|
67 |
|
68 <li><b>Isabelle/HOOL</b> Object-oriented verification of |
|
69 object-oriented programs |
|
70 |
|
71 <li><b><a href="VerifiCard/">Isabelle/VerifiCard</a></b> Tool-assisted |
|
72 Specification and Verification of JavaCardŽ Programs |
|
73 |
|
74 </ul> |
|
75 |
|
76 <p> |
|
77 |
|
78 <b>Important local information:</b> Students are welcome to |
|
79 participate, see <a href="stud/index.html">Isabelle Projekte für |
|
80 Studenten</a> (in German) for more information. |
|