Overview

Description

CALENDAR DESCRIPTION:

Current topics in programming languages depending on faculty and student interest.

COURSE DETAILS:

In this version of the course, "Proof Theory is to Type Theory as Automated Theorem Provers is to Program Synthesis," we will define, and look at the relationships between, four important fields: Proof Theory, Type Theory, Automated Theorem Proving, and Program Synthesis.

The course begins by introducing the field of proof theory. In this section, we will introduce proof theory with the Sequent Calculus. We will then lead from the Sequent Calculus into Natural Deduction, and demonstrate the differences between classical and intuitionistic math.

We then introduce go into type theory by introducing the simply-typed lambda calculus. Surprise! It's natural deduction. We then go into a few more advanced logics and type theories, to more fully explore the relationship of the two as per the Curry-Howard Isomorphism.

With this background, we pivot into proof search and automated theorem proving. We show how many of these approaches come from proof normalization, and show some approaches for syntactically ensuring that normalization. We then apply these tactics to program synthesis. We show the impact of evaluation / semantics on these techniques, and show some strategies for mitigating the downsides incurred.

COURSE-LEVEL EDUCATIONAL GOALS:

Understand the basics of proof theory
Understand the basics of type theory
Understand the basics of automated theorem proving
Understand the basics of program synthesis
Understand the Curry-Howard Isomorphism

Grading

Materials

MATERIALS + SUPPLIES:

I'll be using online materials when possible. For Proof Theory, I'll loosely follow Structural Proof Theory by Negri and von Plato. For Type Theory, I'll loosely follow Types and Programming Languages by Pierce. However, I strongly recommend against buying these books for this class, as we'll only be reading through a few sections of each. For Automated Theorem Proving, we'll use Frank Pfenning's ATP notes (https://www.cs.cmu.edu/~fp/courses/atp/handouts/atp.ps) and for Program Synthesis, we'll be reading some recent papers in the field.