Course on Inductive Definitions
Summer school on the Foundations of Security
University of Oregon - June 2003

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.

This document was translated from LATEX by HEVEA.