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.