Logical frameworks are the formal systems that underlie proof assistants, such as Twelf, Agda, Coq, Lean, etc. Due to instructor bias, we will focus on the Edinburgh logical framework (LF), a tiny dependently typed calculus. Students will learn how to use Twelf, a proof assistant based on logic programming with LF, as well as the formal definition of LF and some of its metatheory. With time/interest, we may examine Agda or Idris to compare approaches.

Know how to read and write inference rules for type systems. Know what the simply-typed lambda calculus is, and probably have seen a proof about it before (e.g. normalization).

- January 30 (first class) - February 29 (last class)
- Tuesdays and Thursdays
- 10:30am - Noon (Eastern US time zone)

Zoom only. See Zulip or reach out to instructor for link.

Each week consists of two days of classes.

- DAY 1 will be dedicated to some kind of lecture and/or livecoding that participants are invited to follow along with.
- At the end of DAY 1, an exercise or two will be assigned, which participants should try to complete before DAY 2.
- DAY 2 will be dedicated to revisiting the exercises and discussing them. Participants are invited to show their solutions. Possibly more lecture and demonstration will follow, but in a less rigid/more improvised manner.

The course will use Zulip for announcements and discussion outside of synchronous classtime.

- The Twelf Wiki
- Run Twelf in your browser!
- Frank Pfenningâ€™s draft book on Computation and Deduction