CS 720: Logical Foundations in Computer Science

Spring 2024

Course information

Class Schedule

Note: Any lecture titles in future dates are considered tentative.

Date # Lecture Download
Week 1: Reading material: [Basics] | HW1
Tu, Jan 23 01 Introduction
Th, Jan 25 02 Functional programming
Week 2: Reading material: [Induction] | HW2
Tu, Jan 30 03 Proofs by Induction
Th, Feb 1 Lab (no slides)
Week 3: Reading material: [Lists] [Poly] | HW3
Tu, Feb 6 04 Polymorphism
Th, Feb 8 05 Tactics
Week 4: Reading material: [Tactics] | HW4
Tu, Feb 13 06 Tactics
Th, Feb 15 (School closure)
Tu, Feb 20 07 Defining logic connectives
Week 5: Reading material: [Logic] [IndProp] | HW4
Th, Feb 22 08 Defining logic connectives
Tu, Feb 27 09 Inductive propositions
Week 6: Reading material: [IndProp] [ProofObjects] | HW4
Th, Feb 29 10 Proof objects
Tu, Mar 5 Lab
Week 7: Reading material: [Maps] [Imp] [ImpParser] [ImpCEvalFun] [Auto] | HW5
Th, Mar 7 11 Imperative languages
Tu, Mar 12 (School closure)
Th, Mar 14 (School closure)
Tu, Mar 19 12 More automation
Week 8: Reading material: [Equiv] | HW6
Th, Mar 21 13 Program equivalence
Tu, Mar 26 Lab
Week 9: Reading material: [Hoare] [Hoare2] | HW7
Th, Mar 28 14 Hoare Logic
Tu, Apr 2 15 Hoare Logic (continued)
Week 10: Reading material: [Smallstep] | HW8
Th, Apr 4 16 Small-step operational semantics
Tu, Apr 9 Lab
Week 11: Reading material: [Types] [Stlc] | HW9
Th, Apr 11 17 Type systems
Tu, Apr 16 18 Functional languages
Week 12: Reading material: [StlcProp] | HW9
Th, Apr 18 19 Properties of the STLC
Tu, Apr 23 Lab
Week 13: Reading material: [MoreStlc] [Typechecking] [Sub] | HW9
Th, Apr 25 20 How to verify?
Tu, Apr 30 21 Lab
Week 14: Presentations
Th, May 2 22 Lab
Tu, May 7 Lab