|
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 at our group (alphabetical order): |
|
22 |
|
23 <ul> |
|
24 |
|
25 <li> <a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a> |
|
26 <li> <a href="/~berghofe/">Stefan Berghofer</a> |
|
27 <li> <a href="/~kleing/">Gerwin Klein</a> |
|
28 <li> <a href="/~narasche/">Wolfgang Naraschewski</a> |
|
29 <li> <a href="/~nipkow/">Tobias Nipkow</a> |
|
30 <li> <a href="/~oheimb/">David von Oheimb</a> |
|
31 <li> <a href="/~prensani/">Leonor Prensa Nieto</a> |
|
32 <li> <a href="/~pusch/">Cornelia Pusch</a> |
|
33 <li> <a href="/~wenzelm/">Markus Wenzel</a> |
|
34 |
|
35 </ul> |
|
36 |
|
37 |
|
38 <h2>Projects</h2> |
|
39 |
|
40 The main Isabelle related projects at TU Munich are currently: |
|
41 |
|
42 <ul> |
|
43 |
|
44 <li> <b><a href="Bali/">Isabelle/Bali</a></b> Java and JVM |
|
45 formalization --- type system, semantics, compilers |
|
46 |
|
47 <li> <b>Isabelle/HOOL</b> Object-oriented verification of Java |
|
48 programs |
|
49 |
|
50 <li> <b><a href="Isar/">Isabelle/Isar</a></b> Intelligible |
|
51 semi-automated reasoning --- readable formal proof documents |
|
52 |
|
53 <li><b><a href="IOA/">Isabelle/IOA</a></b> Verification of |
|
54 distributed, reactive systems using I/O Automata |
|
55 |
|
56 </ul> |
|
57 |
|
58 <p> |
|
59 |
|
60 <b>Important local information:</b> Students are welcome to |
|
61 participate, see <a href="stud/">Isabelle Projekte für Studenten</a> |
|
62 (in German) for more information. |
|
63 |
|
64 |
|
65 <h2>Isabelle resources</h2> |
|
66 |
|
67 <ul> |
|
68 |
|
69 <li> Isabelle <a href="dist/">distribution area</a> |
|
70 |
|
71 <li> Isabelle online theory library: <a |
|
72 href="library-Isabelle99/">Isabelle99</a>, <a |
|
73 href="library-Isabelle98-1/">Isabelle98-1</a> |
|
74 |
|
75 |
|
76 </ul> |