Special Topics in Computer Science

Type Theory and Formal Methods

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.

**Homework 1:**PDF (50KB). Solutions: see the`cs101_hw1`theory in MetaPRL.**Homework 2:**PDF (54KB). Solutions: see the`cs101_hw2`theory in MetaPRL.**Homework 3:**PDF (40KB). Solutions: PDF (28KB).**Homework 4:**PDF (62KB). Solutions: see the`cs101_hw4`theory in MetaPRL.**Homework 5:**PDF (57KB). Solutions: see the`cs101_lc`and`cs101_int`theories in MetaPRL.**Homework 6:**PDF (83KB). Solutions: see the`cs101_hw6`theory in MetaPRL.**Homework 7:**PDF (59KB). Solutions: see the`cs101_hw7`(part I solutions) and`itt_list2`(part II solutions) theories in MetaPRL.**Homework 8:**PDF (76KB). Solutions: see the`cs101_hw8`theory in MetaPRL.**Homework 9:**PDF (74KB).

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
See the ITT.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
See the ITT.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 See the List type in MetaPRL's
ITT.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). |

- MetaPRL system:
`http://metaprl.org/` - MetaPRL
`QUICKSTART`file:`http://cvs.metaprl.org:12000/cvsweb/~checkout~/meta-prl/editor/ml/QUICKSTART` - MetaPRL
`theories.pdf`file (this file is generated nightly from the latest MetaPRL sources):`http://metaprl.org/theories.pdf`. - Alexei Kopylov. Dependent Intersection: A New Way of Defining Records in
Type Theory:
`http://www.cs.cornell.edu/People/kopylov/papers/dinter/dinter_abstract.htm`. - Aleksey Nogin. Quotient Types: A Modular Approach:
`http://nogin.org/papers/quotients.html` - Alexei Kopylov and Aleksey Nogin. Markov's Principle for Propositional
Type Theory:
`http://nogin.org/papers/markov.html` - Robert Constable. Naïve Computational Type Theory:
`http://www.nuprl.org/html/NaiveTypeTheoryPreface.html`. - Robert Constable. The Semantics of Evidence:
`http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR85-684` - Simon Thompson. Type Theory and Functional Programming:
`http://www.cs.ukc.ac.uk/people/staff/sjt/TTFP/`. - Brief introduction to lambda-calculus:
`http://www.cs.cornell.edu/courses/cs611/2002fa/lectures/lec20.ps` - Henk Barendregt. Lambda Calculi with Types.
`ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z` - "What is Formal Methods":
`http://shemesh.larc.nasa.gov/fm/fm-what.html` - Virtual Library: Formal Methods:
`http://www.afm.sbu.ac.uk/` - UGCS Computer Account Request:
`http://www.cs.caltech.edu/cgi-bin/sysadmin/account_request.cgi`