Im Rahmen des Typelab-Projekts soll ein Werkzeug, das Typelab-System,
geschaffen werden, das es gestattet, größere Systeme zu spezifizieren, zu
entwickeln und Eigenschaften dieser Systeme nachzuweisen. Ein besonderes
Augenmerk wird dabei auf Modularisierung von Spezifikationen und auf
Abstraktionsmechanismen gelegt, durch die eine strukturierte Entwicklungs- und
Verifikationsmethodik ermöglicht wird.
Die Arbeiten stützen sich ab auf eine Typentheorie, den Extended Calculus
of Constructions, in dem unter anderem polymorphe Funktionen, Spezifikationen
bzw. mathematische Theorien und Parametrisierung über Theorien ausgedrückt
werden können. Systeme, die ebenfalls auf dem Konstruktionskalkül oder
verwandten Logiken basieren, sind
Alf,
Coq,
Lego,
YARROW und
Nuprl.
Besonderer Wert wird in dem Typelab-System auf Verständlichkeit und
Handhabbarkeit gelegt. Ähnlich wie das
PVS-System
soll der Benutzer bei Verifikationsaufgaben wesentliche Schritte selbst
vornehmen, während einfachere Beweisverpflichtungen durch leistungsfähige
Entscheidungsprozeduren gelöst werden können. In diesem Rahmen ist unsere
Gruppe am
Schwerpunkt Deduktion
der DFG beteiligt. Außerdem bestehen enge Verbindungen zu dem
Projekt
Verifix
(Verifikation von Compilern).
| Konferenzen, Seminare etc. |
| Berichte, Diplomarbeiten etc. |
| Verweise auf andere WWW-Seiten |
Almost the same page in English 
