This course is designed to provide thorough introduction to research in certified proofs and programs. Certified software consists of an executable program plus a formal proof that the software is free of bugs with respect to a particular dependability claim. With certified software, the dependability of a software system is measured by the actual formal claim that it is able to certify. Because the claim comes with a mechanized proof, the dependability can be checked independently and automatically in a reliable way. The formal dependability claim can range from making almost no guarantee, to simple type safety property, or all the way to deep liveness, security, and correctness properties. Dependent types allow us to specify complex properties and verify statically properties about programs. The course is centered around research papers. As such it has two main goals: first, students will survey dependent types and its influence on programming language design and applications such as proof-carrying code, thereby providing an in-depth overview of the current state-of the art. Second, students will learn how to review and evaluate research papers. Some of the topics to be covered are: Dependent types, Dependently-typed programming (DML, Agda, etc.), Proof-carrying code and other proof-carrying applications,
If you are interested, send me e-mail (bp at cs.mcgill.ca).
Theme of this course
``On theories such as these we cannot rely. Proof we need. Proof!" -- Yoda, Jedi Master
Prerequisites:: This is a graduate course. Undergraduates must get permission from the instructor.