| Lecture notes from first class, 2006-09-13, introduction to Sigma-Pi logic,
discussion of Curry-Howard-Lambek isomorphism. Examples of proofs in Sigma-Pi. |
|
|
| Lecture notes from second class 2006-09-15. Cut theorem and rewritings for Sigma-Pi,
annotations of proofs. |
|
|
| Lecture notes from third class 2006-09-20. Discussion, motivation and
proof of confluence for rewritings for Sigma-Pi. |
|
|
| Lecture notes from fourth class 2006-09-22. Proof that Sigma-PI(A) is a
category when A is a Category. |
|
|
| Lecture notes from fifth class 2006-09-27. Discussion of poly categories
and views as a process. |
|
|
| Lecture notes from sixth class 2006-09-29. Continue
discussion of poly categories, views as a process and relationship
to multiplicative linear logic. |
|
|
| Lecture notes from seventh class 2006-10-04. Work
through "boxing" of a graph and the proof of Girard's
switching theorem. |
|
|
| Lecture notes from eighth class 2006-10-06. Discuss
"Empires" and switch conditions. |
|
|
| Lecture notes from ninth class 2006-10-11. Discuss
categorical semantics of cut - multiplicative linear
logic. Introduction of Linear Distributive Categories.
Chu construction. |
|
|
| Lecture notes from tenth class 2006-10-13. Discuss
negation in LL, *-autonomous categories, dualizing objects. |
|
|
| Lecture notes from eleventh class 2006-10-25. Discuss
additives of LL, extension of the additive term logic (Cockett, Pastro) |
|
|
| Lecture notes from twelveth class 2006-10-27 (Sean Nichols). Discuss
message passing logic. |
|
|
| Lecture notes from thirteenth class 2006-11-01. Discuss
initial algebras, final co-algebras and how datatypes arise from this. |
|
|
| Final lecture of part 1, fourteenth class 2006-11-03. Continue discussion
of datatypes, Bekic lemma, circular definitions. |
|
|
