On Tuesday 07/12/2010, at 10h30, in room Byron Blanc.
Speaker: Yves Bertot.
Title: Mixed induction and coinduction.
Abstract:
Several experiments show that data-types where one mixes co-induction and induction can be useful for programming. In particular, this makes it possible to describe the productivity of some algorithms that do not satisfy the coinduction guardedness criterion enforced by the Coq system. In this talk, we will concentrate on a particular description of the Fibonacci sequence, which is semantically well-formed, but which does not satisfy the guardedness criterion, and we will show how this sequence can be modeled using a mix of plain Coq co-recursion and recursion on an ad-hoc inductive predicate.
