Induction and Coinduction in fibrations

Add to your list(s) Download to your calendar using vCal

• Clément Fumex, University of Strathclyde
• Friday 18 November 2011, 16:00-17:00
• LG52 Learning Centre.

If you have a question about this talk, please contact Paul Levy.

In this talk we present inductive and coinductive reasoning principles from the point of view of category theory. We use a fibration to represent the setting of a logic above a type theory. We then start from the well known initial algebras/terminal coalgebras account of inductive and coinductive definitions and look how we can associate to such a definition in the type theory a corresponding reasoning principle in the logic. We finish with a look at possible instantiations of these principles for indexed (co)inductive types.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG52 Learning Centre
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.