Schedule

  • Event
    Date
    Description
    Course Material
  • Lecture
    09/08/2021
    Wednesday
    Introduction

    We’ll talk about what Lean is and see what it can do, and also go over some organizational points about the course.

    Takeaways: verified programming is fun and powerful, and this course is very experimental!

  • Lecture
    09/13/2021
    Monday
    The basics of Lean syntax

    In this lecture we’ll learn the basics of the Lean programming and specification language: types and terms, type inhabitation, and writing and evaluating very simple functional programs. No proving yet!

    We covered HHG 1.1 and 1.2.

  • Assignment
    09/13/2021
    Monday
    Assignment #1 released!
  • Lecture
    09/15/2021
    Wednesday
    The basics of Lean syntax, continued

    We’ll finish Chapter 1 of the HHG, and get a head start on Chapter 2, where we’ll actually start proving some theorems. Today’s topics: inductive types (continued), function definition and evaluation, specifications, and basic tactics. We talked about intro and apply, and how tactic mode is like a proving minigame.

    More on Chapter 2 next time!

  • Lecture
    09/20/2021
    Monday
    Backward (tactic) proofs

    We’ll dive into the meat of the HHG Ch. 2: what are some of the moves available to us in the tactic proving minigame, beyond intro and apply? How do we deal with logical connectives: and, or, not, and so on?

  • Assignment
    09/20/2021
    Monday
    Assignment #2 released!
  • Lecture
    09/22/2021
    Wednesday
    Backward (tactic) proofs, continued

    We’ll continue talking about tactic proofs. How do we deal with equality? What about the natural numbers?

    We’ll also talk about classical vs constructive logic.

  • Due
    09/22/2021 15:00
    Wednesday
    Assignment #1 due
  • Lecture
    09/27/2021
    Monday
    Forward proofs

    We’ll see another way to write proofs in Lean, incorporating forward reasoning.

    Structured (“proof-term”) proofs are a little closer to the underlying logic. Surprise: proofs in Lean are, literally, just terms in the type theory.

  • Assignment
    09/27/2021
    Monday
    Assignment #3 released!
  • Lecture
    09/29/2021
    Wednesday
    Dependent types

    The type theory that Lean is based on, the Calculus of Inductive Constructions, is an instance of dependent type theory. In DTT, we follow the PAT principle: propositions as types, proofs as terms. (Buzzword: the Curry-Howard correspondence!) We’ll look deeper today into these foundations.

  • Due
    09/29/2021 15:00
    Wednesday
    Assignment #2 due
  • Lecture
    10/04/2021
    Monday
    Functional programming: data structures

    Chapter 4 of the Hitchhiker’s Guide introduces some paradigms – inductive types, structures, recursive definitions, type classes – that might be familiar from other functional programming languages. The interesting thing for us is how these paradigms interact with writing proofs. For instance, how do we mix properties into data structures?

  • Assignment
    10/04/2021
    Monday
    Assignment #4 released!
  • Lecture
    10/06/2021
    Wednesday
    Functional programming: type classes, lists, trees

    Type classes are a language feature inspired by Haskell with equivalents in Scala, ML, and other languages. They allow us a kind of ad hoc polymorphism: we can define functions on types that implement certain interfaces, and can declare that certain types implement these interfaces, without bundling the interfaces into the data type itself.

    We’ll see how this interacts with some of the data structures we like to use, as we implement and specify functions on these types.

  • Due
    10/06/2021 15:00
    Wednesday
    Assignment #3 due
  • No Lecture
    10/11/2021
    Monday
    Indigenous Peoples' Day
  • Lecture
    10/13/2021
    Wednesday
    Inductive predicates

    We’ll cover ch. 5 of the Hitchhiker’s Guide today, on inductive predicates. This will complete what we need to know about foundations for now: inductive predicates give us a way to introduce new propositions and prove things about them.

    Inductive predicates are also the source of most of the propositional symbols we’ve used so far – and, or, exists, eq, ….

  • Due
    10/13/2021 15:00
    Wednesday
    Assignment #4 due
  • Lecture
    10/18/2021
    Monday
    Big-step operational semantics

    We’re jumping ahead to Chapter 8 today! Time to start putting what we’ve learned into practice. We’ll define the syntax of a toy programming language inside of Lean, discussing the difference between shallow and deep embeddings. Using inductive predicates, we’ll define a transition system and use this to prove things about the execution of programs in this toy language.

  • Assignment
    10/18/2021
    Monday
    Assignment #5 released!
  • Lecture
    10/20/2021
    Wednesday
    Small-step operational semantics

    The big-step semantics we saw on Monday aren’t fine-grained. We can’t reason about intermediate states. An alternative is using a small-step semantics, where our program execution path is broken down much further. This comes with upsides and downsides.

  • Lecture
    10/25/2021
    Monday
    Lecture
  • Lecture
    10/27/2021
    Wednesday
    Lecture
  • Due
    10/27/2021 15:00
    Wednesday
    Assignment #5 due
  • Lecture
    11/01/2021
    Monday
    Lecture
  • Lecture
    11/03/2021
    Wednesday
    Lecture
  • Lecture
    11/08/2021
    Monday
    Lecture
  • Lecture
    11/10/2021
    Wednesday
    Lecture
  • Assignment
    11/14/2021
    Sunday
    Final project released!
  • Lecture
    11/15/2021
    Monday
    Lecture
  • Lecture
    11/17/2021
    Wednesday
    Lecture
  • Lecture
    11/22/2021
    Monday
    Lecture
  • No Lecture
    11/24/2021
    Wednesday
    Thanksgiving break
  • Lecture
    11/29/2021
    Monday
    Lecture
  • Lecture
    12/01/2021
    Wednesday
    Lecture
  • Lecture
    12/06/2021
    Monday
    Lecture
  • Due
    12/12/2021 23:59
    Sunday
    Final project due