Types, and type systems.
Preliminaries
Lectures
Implementing a language evaluator
Preliminaries
Write you a Kanren for great good!
Meet w/me if you have not.
Our first Kanren
Logic Programming in miniKanren
A Whole New World
Transition
BONUS! Old Proofs, New Topics
Recap Accumulator Reasoning
Check-in, Discussion, Show proofs
Adjusted Schedule
Check-in, Discussion, proofs, Show
Q: How are you all?
Generalization, but really, no.
This isn’t something I have much exciting to talk about.
Induction like a Pro
Induction like a pro: not so hard!
The Trinity
PollE Q to start w/
Induction, Proving Properties w/
HW Setup Q
More Undecidability/Halting Results + Induction
Continuation
Common Recursion Schemes
Proposal Status update.
Measures, Actually
Proposals in; met with most groups;
Definition and Termination
Welcome Back!
Lec13
How to Prove it:
Projects layout plus pen-and-paper proofs
Admin Stuff
Lec11
Where we last left.
Lec10
Where we last left. (Generally)
Lec9
Where we last left. (Generally)
Lec8
A first example: 536 + 487 = 586 + 437
Decision Problems
Valid formulae
Propositional Logic
Reading
(Remainder) of the Dirty Dozen
Reading
Starting ACL2 in Earnest
What questions do we have: here or the audience at home.
A first dose of ACL2
lec2.lisp lec2.lisp.a2s
About the course
Headlines