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
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
Week 7: Reading material: [Maps] [Imp] [ImpParser] [ImpCEvalFun] [Auto] | HW5
Tu, Mar 5 11 Imperative languages
Th, Mar 7 12 More automation
Tu, Mar 12 (School closure)
Th, Mar 14 (School closure)
Week 8: Reading material: [Equiv] | HW6
Tu, Mar 19 13 Program equivalence
Th, Mar 21 Lab
Week 9: Reading material: [Hoare] [Hoare2] | HW7
Tu, Mar 26 14 Hoare Logic
Th, Mar 28 15 Hoare Logic (continued)
Week 10: Reading material: [Smallstep] | HW8
Tu, Apr 2 16 Small-step operational semantics
Th, Apr 4 Lab
Week 11: Reading material: [Types] [Stlc] | HW9
Tu, Apr 9 17 Type systems
Th, Apr 11 Lab
Week 12: Reading material: [StlcProp] | HW9
Tu, Apr 16 18 Functional languages
Th, Apr 18 19 Properties of the STLC
Week 13: Reading material: [MoreStlc] [Typechecking] [Sub] | HW9
Tu, Apr 23 20 How to verify?
Th, Apr 25 Lab
Week 14: Presentations
Tu, Apr 30 Presentations
Th, May 2 Presentations
Tu, May 7 Presentation