Topics in general recursion and interactive theorem proving

Prof. Dr. Vladimir Komendantsky

INRIA Sophia Antipolis, France


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)