►
Logic & Computation
Syllabus
Schedule
Lectures
Homework
Lean Tactic Reference
▼
Lectures
Lecture 1:
Intro
Lecture 2:
Logistics, Specifications in ISL
Lecture 3:
Propositional Logic in Code
Lecture 4:
Design /
Specification Recipe
Lecture 5:
Relational Specifications
Lecture 6:
For-
all, Intro to PBT
Lecture 7:
==>, PBT filtering
Lecture 8:
PBT generators
Lecture 9:
SAT
Lecture 10:
SMT & Rosette
Lecture 11:
Rosette & Finitization
Lecture 12:
Higher order logic
Lecture 13:
Functions
Lecture 14:
Propositional logic
Lecture 15:
Propositional logic & programming
Lecture 16:
Exam 1, Part A
Lecture 17:
Exam 1, Part B
Lecture 18:
Proving with tactics
Lecture 19:
Inductive types & proofs
Lecture 20:
Lists
Lecture 21:
Proof Practice
Lecture 22:
Generalizing hypotheses
Lecture 23:
Generalize
Lecture 24:
Standard Libraries
Lecture 25:
Forward Reasoning
Lecture 26:
Proof Automation
Lecture 27:
Compiler Correctness
Lecture 28:
Induction
Lecture 29:
Functions vs. Relations
Lecture 30:
Why logic?
Lecture 31:
Linear Logic
Lecture 32:
Hoare Logic
Lecture 33:
Separation Logic
Lecture 34:
Exam 2 Review
Lecture 35:
Exam 2, Part A
Lecture 36:
Exam 2, Part B
Lecture 37:
Demo of Slim Check
Lecture 38:
LLMs & Specification
8.7
contents
← prev
up
next →
Lectures
contents
← prev
up
next →