CAS CS 400
Type Theory and Mechanized Reasoning
Boston University
Spring 2024

What is this course?

• Summary:
  
  • give a rough outline of the topics of the course
  • discuss the role of mechanized reasoning in computer science and mathematics
  • look briefly at the Curry-Howard isomorphism
• Reading:
  
  • The Deep Link Equating Math Proofs and Computer Programs (Quanta)
    
  • Mathematicians welcome computer-assisted proof in ‘grand unification’ theory (Nature)
    

Induction and Recursion

• Summary:
  
  • review induction over natural numbers and extend this to induction over inductively-defined sets
  • think about what "kind of thing" induction is, and how that will affect our ability to formalize it
  • discuss the connection between induction and recursion, with any eye towards how these will relate in Lean
• Reading:
  
  • Required:
    
    • TTMR 2: Induction and Recursion
      
    • LAMR 2: Mathematical Background
      
  • Supplementary (Advanced):
    
    • Synthetic Computability (Yannick Forster)
      
    • Bounded Arithmetic (Sam Buss)
      
    • Transfinite Induction (Wikipedia)
      

Agda I: An Introduction

Agda II: Dependent Types

• Summary:
  
  • play with dependent types, with the goal of seeing some of their strangeness, not necessarily understanding how they work
  • start to think about how dependent types can be used to represent "properties" and how that might be useful for mechanized reasoning
• Reading:
  
  • PPA 2: Dependent Types

Propositional Logic I: An Introduction

• Summary:
  
  • discuss in more detail the standard workflow of Agda
  • introduce the syntax and semantics of propositional logic (as well as what exactly these terms mean)
  • see how we can use Agda as a framework for implementing propositional logic
• Reading:
  
  • Required:
    
    • TTMR 4: Classical Propositional Logic
      
      • 4.1: Syntax
        
      • 4.2: Semantics
        
  • Supplementary:
    
    • A Primer on Propositional Logic
      
    • Propositional Logic
      
    • LAMR 4: Propositional Logic
      

Propositional Logic II: Meta-Theory

• Summary:
  
  • dive deeper into pattern matching in Agda, introducing with-abstraction for pattern matching on intermediate computations
  • introduce semantic notions in logic, particularly up to the notion of logical equivalence
• Reading:
  
  • Required:
    
    • TTMR 4: Classical Propositional Logic
      
      • 4.3: Meta-Theory
        
      • 4.4: Functional Completeness
        
  • Supplementary:
    
    • LAMR 4: Propositional Logic
      

SAT-Solvers I: An Introduction

• Summary:
  
  • finish discussing semantics notions in propositional logic
  • talk about functional completeness and normal forms
  • introduce SAT solvers and the DPLL procedure
• Reading:
  
  • Required:
    
    • TTMR 4: Classical Propositional Logic
      • 4.5: Conjunctive Normal Form
    • TTMR 5: SAT Solvers
      • 5.1: Restriction
      • 5.2: DPLL
  • Supplementary:
    
    • LAMR 6.2: Unit Propagation and the Pure Literal Rule
    • LAMR 6.3: DPLL

SAT-Solvers II: In Practice

• Summary:
  
  • look at a couple encodings of propositions as CNF formulas
  • look at an example application of SAT-solvers
• Reading:
  
  • Required:
    
    • TTMR 5: SAT Solvers
      • 5.3 CNF Encodings
      • 5.4 Example: Sudoku
  • Supplementary:
    
    • LAMR 7: Using SAT Solvers

Propositional Proofs

• Summary:
  
  • define the notion of a proof system and a Gentzen-style sequent proof
  • introduce resolution as an example of a proof system
  • demonstrate the connection between resolution and DPLL.
• Reading:
  
  • LAMR 8.2: Resolution
  • LAMR 8.4: Resolution and DPLL

The Lambda Calculus I: An Introduction

• Summary:
  
  • introduce the syntax and semantics of the lambda calculus.
• Reading:
  
  • TTFP 2: Functional Programming and Lambda-Calculi
    • 2.2: The untyped lambda-calculus
    • 2.3: Evaluation

The Lambda Calculus II: Meta-Theory

• Summary:
  
  • introduce semantic notions of the lambda calculus, including normalization and evaluation strategies.
  • look at how to encode data.
  • talk breifly about De Bruijn indices and alpha equivalence.
• Reading:
  
  • TTFP 2: Functional Programming and Lambda-Calculi
    • 2.4: Convertibility
    • 2.5: Expressiveness

Simple Types I: An Introduction

• Summary:
  
  • introduce the simply typed lambda calculus (STLC)
  • give an outline of the proof that STLC is strongly normalizing
• Reading:
  
  • TTFP 2: Function Programming and Lambda-Calculi
    • 2.6: Typed lambda-calculus
    • 2.7: Strong normalization
  • Strong Normalization for Simply Typed Lambda Calculus (Notes)

Simple Types II: The Curry-Howard Isomorphism

• Summary:
  
  • finish the discussion of strong normalization
  • discuss data types in STLC
  • connect data types to the Curry-Howard isomorphism
• Reading:
  
  • TTFP 2: Function Programming and Lambda-Calculi
    • 2.8: Further type constructors: the product
    • 2.9: Base types: natural numbers
  • PPA 3.1: The Curry-Howard correspondence: Propositional logic

Agda III: The Proof Assistant

• Summary:
  
  • recall the Curry-Howard isomorphism and see how it applies to Agda
  • see how to interpret Agda programs as mathematical proofs and translate mathematics into Agda
• Reading:
  
  • PPA 3: The Curry-Howard correspondence (whole chapter)

Agda IV: Equational Reasoning

• Summary:
  
  • discuss how to prove complex equalities in Agda
  • see many examples in code
• Reading:
  
  • PPA 4: Equational reasoning in Agda (note: we use different syntax, but the ideas transfer)

Case Study I: STLC in Agda

• Summary:
  
  • see how to formalize the simply typed lambda calculus in Agda
  • prove several meta-theoretic lemmas, leading to type preservation
• Reading:
  
  • look through the code from lecture

Case Study II: Verified Sorting

• Summary:
  
  • verify that (functional) insertion sort returns an ordered list
  • see the connections between how the algorithm is written and how properties are proved about it
• Reading:
  
  • look through the code from lecture

Intuitionistic Logic I: An introduction

• Summary:
  
  • introduce a proof system for intuitionistic propositional logic with propositional variables (IPL) as the simply typed lambda calculus with type variables with type variables (STLC) minus the computational content
  • introduce a proof system for classical propositional logic (CPL) as IPL plus a variant of proof by contradiction
  • look at classical principles which are not intuitionistically provable
  • see what is gained by thinking intuitionistically (e.g., the disjunction property)
• Reading:
  
  • please look through the lecture slides

Intuitionistic Logic II: Kripke Semantics

• Summary:
  
  • recall the notions of soundness and completeness
  • note that IPL is not complete with respect to valuations
  • present Kripke models as an alternative semantics for which IPL is sound and complete
  • use Kripke countermodels to prove that some classical principles cannot be proved in IPL
• Reading:
  
  • please look through the lecture slides

Polymorphism I: In Introduction

• Summary:
  
  • look generally the notion of polymorphism
  • introduce System F as a typed lambda calculi with polymorphism
  • discuss briefly the role of type annotations in type checking and type inference
• Reading:
  
  • please look through the lecture slides

Polymorphism II: Logic in System F

• Summary:
  
  • recap System F
  • look at how to represent logical connectives in System F
  • briefly discuss unification, implicit variables, and the type inference problem

Dependent type theory I: An introduction

Dependent type theory II: Meta-Theory

Advanced: Type-theoretic paradoxes