|University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence||up: Research|
|Fast diesselbe Seite auf Deutsch|
The long-range purpose of the Typelab project is to create an environment that permits to specify large systems and to verify properties of these systems. A structured development method and good reuse properties are achieved by mechanisms such as modularity of specifications and abstraction.
The formal context of this work is a type theory, the Extended Calculus of Constructions, in which polymorphic functions, specifications, mathematical theories and parameterisation over theories can be expressed.
Currently, the emphasis of the project is on developing an environment which permits specifications to be written in a user-friendly syntax and which provides basic reasoning facilities, such as a sequent calculus prover with an intermediate degree of automation. Another research topic is a knowledge-based proof assistant that exploits previously derived knowledge for making abstract inferences, rather than carrying out proofs on an elementary level.
Related Systems Other systems based on type theories are: Alf, Coq, Lego, YARROW and Nuprl.
HOL and Isabelle are proof systems based on higher-order logic.
The PVS system (also see European mirror site at Ulm) is a very user-friendly verification environment that provides a high degree of automation. One of its distinctive features is a generic module system.
IMPS permits formalization of axiomatic theories and theory morphisms. Specware emphasizes constructions on modules using a categorical formalism.
|Conferences, Workshops etc.|
|Reports, Master Theses etc.|
|Dept. of AI Homepage||Research||Help||Mail to Webmaster||Marko Luther - Feb. 23, 1998|