# Lectures

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

# Instructor

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

)

# Announcements

**Welcome back**: First class is 1 Sep!

# 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.