| Time: | MW 14:00 - 14:55 |
| Place: | Jorgensen 74 |
| Instructor: | Aleksey Nogin |
| Units: | 9 (2+3+4), pass/fail or letter grade |
| Prerequisites: | CS20(a,b) |
| Office Hours: | Jorgensen 70; Mon 3PM, Thu 5:30PM, and by appointment |
| TA: | Xin Yu |
| TA Office Hours: | Jorgensen 160I; Tue 9-11PM |
Instructor and TA contact address: cs101-admin@metaprl.org.
Class mailing list: cs101-class@metaprl.org (web interface).
Class distribution of MetaPRL: meta-prl.tar.bz2, 4.6MB. The current version is 0.8.3 (CS101 rev 12). Please see instructions on how to make sure you are running the latest version.
| Mar 31 | Introduction, Motivation, Propositional Classical Logic. Slides: PDF, 929KB. Proofs: PDF, 41KB. |
| Apr 2 | Semantics and Soundness, Classical Logic, Intuitionistic Logic. Slides: PDF, 467KB. Rule listing: PDF, 30KB. |
| Apr 7 | Introduction to MetaPRL. Rule listing: PDF, 30KB. MetaPRL cs101 theory: CVSWeb listing; Instructions for updating MetaPRL. Listing of CS101 theories: PDF, 89KB |
| Apr 9 | Proof Automation in MetaPRL. Slides: PDF, 501KB. |
| Apr 14 | Introduction to Lambda-Calculus and Meta-Patterns. Slides: PDF, 566KB. |
| Apr 16 | Lecture cancelled because of the Student-Faculty Conference 2003. |
| Apr 21, 23 | Implementing Lambda-Calculus and Basic Type Theory in MetaPRL. Lecture notes: see the cs101_lc theory in MetaPRL. Listing of CS101 theories: PDF, 89KB |
| Apr 28 | Dependent Types. Lecture notes: see the cs101_lc theory in MetaPRL. Listing of CS101 theories: PDF, 89KB |
| Apr 30 | Curry-Howard Isomorphism, Propositions-as-Types. Slides: PDF, 354KB. Proofs: see the cs101_int theory in MetaPRL. Listing of CS101 theories: PDF, 89KB |
| May 5 | Equality in Type Theory. Slides: PDF, 473KB. See also the Itt_equal section of the MetaPRL theories.pdf file. |
| May 7 | Equality and Universes in MetaPRL's ITT. See the itt_equal and itt_struct modules in MetaPRL and the corresponding sections in the theories.pdf file. |
| May 12 | Basic type constructors in MetaPRL's ITT. See the itt_squash, itt_squiggle, itt_subtype, itt_void and itt_unit modules in MetaPRL and the corresponding sections in the theories.pdf file. Optional reading: the "Markov's Principle for Propositional Type Theory" paper explores classical reasoning under squash. |
| May 14 | The List type in MetaPRL's ITT. See the itt_list, cs101_list2 and itt_list2 modules in MetaPRL and the corresponding sections in the theories.pdf file. |
| May 19, 21 | Booleans, esquash, quotient types and collections in MetaPRL type theory. See the itt_bool, itt_esquash, itt_quotient and itt_collection modules in MetaPRL and the corresponding sections in the theories.pdf file. Recommended reading: "Quotient Types: A Modular Approach" |
| May 26 | Memorial Day (Institute holiday) |
| May 28 | Intersection and record types. See the itt_isect, itt_bisect, itt_disect, itt_record and itt_record_exm modules in MetaPRL and the corresponding sections in the theories.pdf file. See also: Dependent Intersection: A New Way of Defining Records in Type Theory. |
| Jun 2, 4 | TBA. Note: these lectures are optional, the material covered in these lectures will not be included in any homework(s) or test(s). |