Research Group on Natural Computing

Prof. Dr. Vladimir Komendantsky

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)