Inductive definitions and type theory an introduction (preliminary version)

We give a short introduction to Martin-L\uf6f\u27s Type Theory, seen as a theory of inductive definitions. The first part contains historical remarks that motivate this approach. The second part presents a computational semantics, which explains how proof trees can be represented using the notations of functional programming