Abstract

As researchers in theory, and in particular, programming language theory, we are interested in theorems and proofs. For high-assurance, we want these to be checkable automatically. Various proof assistants have been devised and used for mechanizing some realistic proofs, as well as challenges such as POP Lmark. The Twelf tool is such a proof assistant, with support for representation of formal systems and inductive proofs over them. It supports and encourages a method of representation known as higher-order abstract syntax, which simplifies reasoning about systems with binding structures and with hypothetical reasoning.

This course is a tutorial introduction to Twelf, in its role as a system for representing formal systems and checking proofs about them. We will look at encodings of systems, proofs about them, and helpful strategies to convince Twelf we have a good proof. We will also learn how to understand a proof we get, and believe in these proofs. Our examples will be drawn from the metatheory of programming languages and type systems.

Course materials will be put here .