5 Project

The final project will be an opportunity for you to further explore areas of formal verification and/or programming languages that you find interesting. This can take the form of either a research report or a project to formally verify something of interest, such as a mathematical theorem or program specification. The project does not have to use Coq; in fact we encourage students to explore other theorem provers. Some alternative proof assistants:

• Isabelle

• LEAN

• Agda

• F-Star

• Dafny

• Liquid Haskell

We also encourage building upon existing software projects such as

• The Mathematical Components Library

• The Iris separation logic

• The QWIRE verified quantum programming language

• The QuickChick random testing tool (also here)

to name a few. Neither of these lists is intended to be exhaustive.

There are also a number of books that may be useful starting points including

• Software Foundations(particularly the volumes we haven’t covered)

• Programming Language Foundations in Agda

• Certified Programming with Dependent Types

Students are welcome to work in pairs, though more will be expected of group projects than solo ones. Project proposals are due on April 2nd, but we encourage you to submit early and get a head start. The final project will be due on May 14th. Students may also volunteer to present their projects during the final classes, though this isn’t required.