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).
Zoom only. See Zulip or reach out to instructor for link.
Each week consists of two days of classes.
The course will use Zulip for announcements and discussion outside of synchronous classtime.