Type Theory Today

[Joseph Razavi]

Hi Everyone,

Today I think most of us will still be thinking about the factorial
exercise. After having done that, the sections Proof By
Simplification, The intros Tactic, Proof by Rewriting, Case Analysis,
and Induction start the really interesting stuff -- the proofs!

The exercises:

simpl_plus
mult_1_plus
zero_nbeq_plus_1
basic_induction

would be good to look at.

See you all later,

Joe


P.S. Those of you who are a bit ahead might be interested in the
general plan. The idea is to do the chapters Basics - Logic. After
this Pierce's course starts to develop the particular theory he's
interested in. If we get that far in a semester, we'll go on to
explore some advanced issues about Coq's type system. If you'd like to
get ahead that's great; I'd be happy for people to have questions
about any of that material in the sessions, and you could help guide
the process for everybody else!