## General recursion in type theory

Projet Lemme

INRIA Sophia Antipolis

Thursday, 4 September 2003, 12:00 (note the unusual time!)

Cybernetica Bldg (Akadeemia tee 21), room B101

**Abstract**: Constructive type theory is an expressive
programming language where both algorithms and proofs can be
represented. However, general recursive algorithms have no direct
formalisation in type theory since they contain recursive calls that
satisfy no syntactic condition guaranteeing termination.

I will describe a method by Ana Bove and myself to represent
general recursive functions in type theory. It consists in generating
simultaneously a domain predicate and the recursive definition of the
function. To do this we need Dybjer's simultaneous inductive-recursive
definitions. I will discuss how these can be represented in the
Calculus of Constructions.

Another method models possibly infinite computation by a
coinductive type. I will compare the two methods and discuss how they
can be integrated.

Tarmo Uustalu

Last update 11.8.2003