TuTh 9:35am-10:55pm, ENGMC 103 (new)


Prof. Brigitte Pientka (bpientka at cs dot mcgill dot ca)


Themes of the Course

Dependent types allow us to track rich properties about the (partial) correctness of a program as part of the type. Such properties can then be verified statically via type checking prior to running the program. The power of this idea is far reaching: we can statically verify termination of many programs, check for array-bounce or track access control policies. In addition to checking rich properties statically, dependent types also allow us to certify that a program satisfies a given property allowing the programmer to construct and return an explicit proof object which can be validated independently.

The course begins with a theoretical introduction to dependent types. We then survey the landscape of dependently typed programming and proof environments, its use in logical frameworks to represent proofs and explore its applications in proof-carrying code and mechanizing the meta-theory of formal systems.

Note: This is a research seminar, not a lecture course. Participants are required to present several papers during the course of the semester and participate in the online and in-class discussion. Each presentation must be accompanied in advance by typeset lecture slides in either Powerpoint or LaTeX slide format. The presenter's slides will be posted on the course web site for future reference. The presenter is responsible for presenting a summary and a critical analysis of the paper(s) assigned to her, and to lead discussion. The audience for a given paper is required to read the relevant papers in advance as preparation for the presentation.

Prerequisites: This course is for graduate students and advanced undergraduates who wish to pursue research in programming languages and type systems. It will assume a basic knowledge of types and functional programming (at the level of COMP-302). Ideally students should also have taken some of the following courses: PHIL 310, COMP 523, COMP 527. Familiarity with B. Pierce "Types and Programming Languages" (Ch 1 - Ch 11) will be assumed.