Syllabus

Introduction

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.

Course Material

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.

Logistics

Students and auditors from Boston University and nearby universities are all welcome.

Instructors: Assaf Kfoury with the assistance of Kinan Dak Albab.

Meeting times and places: Lectures on Foundations on Tuesday and Thursday, 11:00 am - 12:15 pm, in Room PSY B39. 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.

Homework and Project Logistics

Foundations: Homework on foundations will be assigned every two weeks, to be handed in after two weeks. The homework consists of pen-and-paper exercises on foundations. Each homework will have optional exercises you can solve for extra credit.

Pragmatics: There will be four pragmatics homework through out the course. The last pragmatics homework will be due on March 27. Pragmatics homework will be made out of small programming and modeling exercises in our four systems. These exercises will be drawn out of different areas of Computer Science. You are allowed to choose some threshold of these problems to solve, according to your areas of interest. You can solve all of them for extra credit.

Project: Project proposals are due March 27, and the projects themselves are due on May 11th. Proposals are expected to be 1-2 pages, outlining the general problem, providing some motivation for it, and listing out what techniques or tools you plan on using. Final project submissions must consist of a report for projects emphasizing on foundations, or relevant code and automated proofs with a smaller report summarizing the results.