Spring 2004

Randy Pollack, office 2608, email: rap @ inf

Thursday 18/03 - 08/04 13.30 - 14.30 JCMB 3315

Tuesday 20/04 14.30 - 15.30 JCMB 6207

Thursday 22/04 13.30 - 14.30 JCMB 6310

- Accumulated lecture notes, including a bibliography with suggested reading.

- Other notes of possible interest.
- The Church-Rosser theorem: a short note, slides.
- Names, binding and alpha conversion.
- Formal proof in LEGO of weak normalization of MIL using Tait computability method. This is the simplest use I know of Tait computability.

- (16/3/04) (First 2 sections of Accumulated lecture notes.) A preview of two main ideas: the Curry-Howard correspondence, and the duality between introduction and elimination, with structural recursion being the induced computation. We then begin with minimal implicational logic (MIL).
- (18/3/04) Through section 3, normalization of MILT.
- (23/3/04) Hopefully sections 4 - 7.
- (25/3/04) Hopefully sections 7 - 9.
- (30/3/04) Hopefully sections 10 - 13.
- (1/4/04) Sections 12 - 14.
- (6/4/04) Sections 15 - 16.
- (8/4/04) Sections 16 - 17.
- (13/4/04) and (15/4/04) NO LECTURES.
- (20/4/04) Finish section 17, begin section 19. (Skipping section 18.) ROOM JCMB 6207!
- (22/4/04) Section 19. (Skipping section 18.) ROOM JCMB 6310!!