INSTITUTE of CYBERNETICS at TTU

Spring Lectures in Mathematical Logic

Speaker:	Dr. Anton SETZER, University of Uppsala, Sweden, and University of Swansea, UK
Place:	Room B 216, Institute of Cybernetics, Akadeemia tee 21, Tallinn, Estonia
Time:	Monday, May 14, 2001, 14:00

---

DEPENDENT TYPE THEORY
AND INDUCTIVE-RECURSIVE DEFINITIONS

Abstract

In the first part of this talk we will give an introduction to Martin-Loef Type Theory. We will start with the foundational problems which led to the design of dependent type theory and will give an overview over the standard sets (data structures) in this theory. Then we will indicate how type theory can be used as a programming language. Finally, we will investigate the common pattern behind the set constructions in type theory, and arrive at the concept of inductive-recursive definitions as an abstract concept for defining all these sets.

If time permits we will show how to introduce a closed formulation of inductive-recursive definitions and indicate how this can be used in generic programming.

---

Dr. Sergei Tupailo
Institute of Cybernetics at TTU
Akadeemia tee 21, 12618 Tallinn, Estonia
email: sergei@cs.ioc.ee