Next: About this document
Up: Class note 28
Previous: Cartesion Product
Consider our 
-terms LT with the operators
and 
. We might ask the following questions:
Does Subject Reduction still hold?
Does termination still hold?
Does Church-Rosser still hold?
It can be shown that the answer is 'yes' in all of these cases.
Whenever we extend our type system, as we did with the Cartesian Product,
we should see how it affects the syntax, the computation rules (in terms
of rewrite and structured operational semantics) and the typing rules
(including Subject-Reduction, Church-Rosser and termination.)
Next: We start on Chapter 5 of Gunter and begin discussing modules and
dependent types.