| Main page |
| Members |
| Events |
| Visitors |
The ULTRA group
The Name
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 biological systems.
Logics
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 computational feasibility.Types
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
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.Automation
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 computer systems.Research efforts we are part of
- SESAME: Semantic Structure for Managing Mathematical Knowledge
- The Church Project
- The DART Project
- The MKM Network