The ULTRA group
We chose to name ourselves "ULTRA" because this word contains
"L" for Logic, "T" for Types, "R" for Rewriting, and
"A" for Automation.
Active research in logic,
types, and rewriting is improving the safety, reliability,
security, and capability of many kinds of software systems
including the design and implementation of programming
languages. Research in these areas is also vital in the
formalization of mathematics and automated theorem proving.
There is also an increasing use of logic, types, and rewriting
for describing, understanding, and managing business systems and
Logic is the basis for any kind of rigorous reasoning in
Mathematics and Computer Science, e.g., proving the correctness
and safety of computer programs. Different logics have
different properties and there is an ongoing search for better
logics with better combinations of expressiveness and
Types support increasing the expressiveness of programming
languages and logics without losing important theoretical
properties. Thus, types are the foundation of safe
(paradox-free) logics and safe programming languages.
Rewriting is a method for applying the rules of logic,
mathematics, or computation in a stepwise manner. This is used
in reasoning about efficient computation strategies and
equivalences between logical propositions or computer programs.
Theoretical results in logics, types and rewriting are
especially suitable for automation. A vital part of testing and
evaluating new results is to implement them in automated
Research efforts we are part of
Can be found on the individual home pages of each