INRIA Sophia Antipolis, France

**Abstract:**

In my talk I briefly introduce a powerful proof assistant Coq, one of the most widely used automated

theorem proving tools today.

I illustrate the uses of Coq by providing several methods allowing to incorporate general recursive

(e.g., potentially non-terminating) recursive functions inside the underlying theory of this proof assistant.

The most prominent point is that the theory, does not lend itself to such functions. Still one

can constructively reason about general recursion using bounded recursion, well-founded inductive

definitions or coinductive notions of computation.

The latter is illustrated by the construction of Kahn networks. I also show what classical axioms allow

to define general recursive functions in the Logic of Computable Functionals.

- Date: July 18th 2008, at 13h
- Place: Seminar room of the Department (ETSII, Module H, First floor)