# Programs and Proofs

## Course Objectives

This course is about an approach to bringing software engineering up to speed
with more traditional engineering disciplines, **providing a mathematical
foundation for rigorous analysis of realistic computer systems**. As civil
engineers apply their mathematical canon to reach high certainty that bridges
will not fall down, the software engineer should apply a different canon to
argue that programs behave properly.

As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments and solver-aided languages that automatically verify logical arguments. We will learn how to apply these tools to certify that programs behave as expected.

Specifically, we will look at

- Formal logical reasoning about program correctness through
- Coq proof assistant, a tool for machine checked mathematical theorem proving and
- F*, a general-purpose programming language aimed at program verification

**Is this a program verification course?**

Yes, but let’s stick to Program Proofs.

## Course Contents

**Foundations:**Induction principles, logic and propositions, Curry-Howard correspondence.**Specification and Verification:**Program Equivalence – Transition Systems – Operational Semantics - Compiler Verification – Model Checking – Simply Typed Lambda Calculus.**Program Logics:**Hoare logic: an approach to verifying imperative programs - Separation logic: reasoning about aliasing and pointer-based data structures.**Programming with F*:**Programming in F* - Inductive Types - Verified Functional Programming – Termination - Programming with Effects**Proving with F*:**Verifying Stateful Programs – Dijkstra Monad - Higher Kinds, Indexed Types, Type-level functions – Cryptography examples - Verifying low-level code using Low*, a subset of F***Concurrency:**Concurrent Separation Logic and rely-guarantee reasoning: verifying concurrent shared-memory programs - Pi-calculus and behavioral refinement: modular reasoning about message-passing functional programs – Session Types for distributed programming.

## Class info

Location: CS26 Time:

- M 1100 - 1150
- Tu 1000 - 1050
- W 0900 - 0950
- Th 1200 - 1250

## Credits

3-1-0-0-8-12

## Evaluation Plan

- Weekly Assignments: 60%
- Midterm: 20%
- Finals: 20%

## Pre-requisite

CS3100 (only the OCaml parts) or equivalent.

You should feel comfortable with functional programming concepts. If you are able to get through the assignments 1 to 4, you are ready for this course. All the course materials, and assignments are available on the CS3100 website.

**I highly recommend that you complete assignments 1 to 4 before the start of
this course**.

If you are unsure, please come talk to me.