►
Logic & Computation
Syllabus
Schedule
Office Hours
Lectures
Homework
▼
Lectures
Lecture 1:
Intro
Lecture 2:
Logistics, Specifications in LSL
Lecture 3:
Propositional Logic in Code
Lecture 4:
Using LSL
Lecture 5:
Design /
Specification Recipe
Lecture 6:
Using LSL II
Lecture 7:
Using LSL III
Lecture 8:
Relational Specifications
Lecture 9:
Dependent Contracts
Lecture 10:
Itemizations
Exam 1
Lecture 12:
Recursive Contracts
Lecture 13:
More Recursive Data
Lecture 14:
Continuing with Recursive Data
Lecture 15:
Specifications with Functions
Lecture 16:
Polymorphism
Lecture 17:
Polymorphism II
Lecture 18:
Programming Against Interfaces
Lecture 19:
Finitizing, Rosette
Lecture 20:
Recursion & Induction
Lecture 21:
Temporal Specifications
Exam 2
Lecture 23:
Reasoning about Mutable State
Lecture 24:
Value Mutation
Lecture 25:
More Pointer Equality
Lecture 26:
Concurrency
Lecture 27:
Concurrency II
Lecture 28:
Concurrency Lab
Lecture 29:
Big-
O
Lecture 30:
More Performance
Lecture 31:
Visualization for Concurrency
Lecture 32:
Resources
Lecture 33:
Introduction to Proof
Lecture 34:
Proofs with Propositional Logic
Lecture 35:
Proofs with Tactics
Exam 3
Lecture 37:
Inductive types/
proofs, Proof automation
Lecture 38:
LLMs & Specification
8.11
contents
← prev
up
next →
Lectures
contents
← prev
up
next →