We introduce inductive types, which allow for a natural description of most of the data structures used in both computer science and logic, such as inductive sets à la ML (e.g. trees, lists, natural numbers). Besides the syntactic aspect of inductive definitions, is the computation part, recursion, and the logical part, induction. The expressivity of the different recursion and induction principles will be discussed. Definitions by induction are also convenient to define logical properties as least predicates satisfying some closure properties.

• Slides (advi) (ps) for slides on a page
• Coq file for the example of cryptographic protocol
• Coq file for the example of proof by reflexion

This document was translated from L^AT_EX by H^EV^EA.