Description

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.

Lectures

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

Instructor

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

Office Hours

Background Reading

The following is on reserve in the Schulich library.

Reading

This is a research seminar, not a lecture course. Lectures will be organized around the discussion of one or more research papers taken from the conference proceedings and journals in the area of programming languages, logic, and type theory. The reading list is posted on the schedule.

Evaluation

Important dates

Mid-term report due, Oct 13

Mid-term reviews due, Oct 20

Final report due, 29 Nov

Workshop day, Dec 1

Language Rights

In accord with McGill University's Charter of Students' Rights, students in this course have the right to submit in English or in French any written work that is to be graded.

Academic Integrity

McGill University values academic integrity. Therefore all students must understand the meaning and consequences of cheating, plagiarism and other academic offenses under the Code of Student Conduct and Disciplinary Procedures (see http://www.mcgill.ca/integrity/ for more information). Most importantly, work submitted for this course must represent your own efforts. Copying assignments or tests from any source, completely or partially, or allowing others to copy your work, will not be tolerated.