Foundations and Pragmatics of Dependently-Typed Systems for Interactive Proof-Assistance and Certifiably-Safe Programming
The need to certify ever-more complex software artifacts has spurred an unprecedented development of methodologies for analysis and verification based on principles of mathematical logic. The overarching goal is to ascertain that software artifacts, which implement complex algorithms or model interacting processes in wider computing environments, satisfy formally specified properties (typically related to safety or security, but not only). Success of these formal methodologies in real-world applications has depended on their being automated, partially or fully, and on their scaling up to large software packages beyond the ability of human agents to analyze and verify by hand.
We will look at the foundations and pragmatics of four mature systems: Coq, Agda, Lean, and ATS. While Coq and Lean are primarily interactive proof assistants, Agda and ATS aim to create environments for certifiably safe programming. Nevertheless, all four systems can be used for both purposes, as well as combinations of them. These four systems share a common theoretical core, primarily based on what are called dependently-typed lambda-calculi. Our selected four are excellent representatives of the benefits provided by advanced type-based frameworks, but they also diverge significantly in many other respects, both in their theoretical foundations and in their pragmatics.
Foundations: About 2/3 of the course will be devoted to foundational aspects of the systems under consideration. We will start briefly with background material on Lambda Calculus, Simple Type Theory, and First Order Logic, moving into the core material on Curry-Howard Isomorphism, Dependent Types, and the Calculus of Inductive Constructions. We will conclude with an introduction to Homotopy Type theory as time permits.
Pragmatics: About 1/3 of the course will be devoted to the pragmatics of the four systems, which will run concurrently to the portion on foundations. We will cover the basics of using these systems with examples from: Safe Systems Programming, Computer-Aided Cryptographic Proofs, Formally-Certified Compilers, and many others from across the computer-science field.
Other Systems: These four systems are a small selection from at least a dozen currently available dependently-typed systems (see the Wikipedia pages Proof Assistant and Dependent Type for partial lists). Additionally, not all interactive proof assistants are based on the same theoretical foundations. In particular, there is a successful competing group of systems based on higher-order logic (see LCF and its successors) which we will not cover.
Students and auditors from Boston University and nearby universities are all welcome.
Meeting times and places: Lectures on Foundations on Tuesday and Thursday, 11:00 am - 12:15 pm, in Room MCS B25. Lab Tutorials on Pragmatics on Wednesday, 4:40 pm - 5:30 pm, in Room MCS B08.
Online discussion: We will use Piazza for announcements, queries from students to the teaching staff, and queries between students. You will get an email from Piazza with a link inviting you to create an account within the first week of the Spring 2019 semester.
Evaluation: Students are expected to meet a set minimum understanding of both foundations and pragmatics, but are free to focus on one (or both) according to their interests. Evaluation will be entirely based on Homework and Project. We will have bi-weekly homework on foundations (consisting of pen-and-paper proof exercises), and on pragmatics (examples from different areas of Computer Science to be implemented in a particular system).
Project: Students can choose projects ranging from the theoretical foundations, the pragmatics of implementing a complicated example, or a comparative study between several of the systems on a smaller example. Flexibility in the project is intentional, to give students the ability to focus on their individual interests.