►
Logic & Computation
Syllabus
Schedule
Office Hours
Lectures
Homework
ISL+
Recap
▼
Lectures
Lecture 1:
Intro
Lecture 2:
Logistics, Specifications in LSL
Lecture 3:
Propositional Logic in Code
Lecture 4:
Using LSL
Lecture 5:
Using LSL II
Lecture 6:
Design /
Specification Recipe
Lecture 7:
Relational Specifications
Lecture 8:
Dependent Contracts
Lecture 9:
Itemizations
Lecture 10:
Recursive Contracts
Lecture 11:
More Recursive Data
Lecture 12:
Continuing with Recursive Data
Lecture 13:
Using LSL III
Lecture 14:
Specifications with Functions
Lecture 15:
Polymorphism
Lecture 16:
Polymorphism II
Lecture 17:
Data Abstraction in OO Languages
Lecture 18:
Programming Against Interfaces
Exam 1
Lecture 20:
Recursion & Induction
Lecture 21:
Reasoning about Mutable State
Lecture 22:
Value Mutation
Lecture 23:
More Pointer Equality
Lecture 24:
Temporal Specifications
Lecture 25:
Concurrency
Lecture 26:
Concurrency II
Lecture 27:
Concurrency Practice
Lecture 28:
Big-
O
Slack Day
Lecture 30:
More Performance
Lecture 31:
State Machines
Lecture 32:
Resources
Special Topics:
Interactive Theorem Proving with Rocq
Special Topics:
Verification with Dafny
►
Slack Day
1
Purpose
On this page:
1
Purpose
8.15
contents
← prev
up
next →
Slack Day
🔗
1
Purpose
🔗
Different sections did different things.
contents
← prev
up
next →