[Tutorial Fest @ POPL'23] Using a Proof Assistant to Teach PL Theory, Without the Overhead

Jonathan Aldrich and John Boyland demonstrate how to use the SASyLF proof assistant to teach programming language theory with minimal overhead.

[TutFest'23] Using a Proof Assistant to Teach PL Theory, Without the Overhead Jonathan Aldrich, John Boyland This tutorial presents an approach to teaching programming language theory with a proof assistant, SASyLF, that gives students immediate feedback on formalisms and proofs but imposes little overhead. SASyLF leverages common “blackboard” teaching notation for syntax, definitions, and proofs; the error messages follow suit. Built-in support for variable binding reinforces key PL concepts and avoids a major learning hurdle present in other proof assistants. While focused on education, SASyLF can be used directly in research, or can be a stepping stone to other tools. The tutorial will go through four assignments of increasing difficulty: formalizing properties of addition, proving equivalence of small-step and big-step semantics, proving type soundness, and proving types are preserved by optimization. Along the way, we’ll show how we introduce the tool to students, and how the tool can help with common student misconceptions. Participants in the tutorial will have time to use the tool on a portion of these assignments to get a sense for the tool’s learning curve and how it works. The assignments used in the tutorial and a written introduction to the tool that synchronizes with these assignments, all used at CMU and suitable for incorporation in other PL courses, are freely available at www.sasylf.org. Participants are encouraged to download SASyLF and the Eclipse IDE plugin from sasylf.org/ before the tutorial and follow along with the interactive exercises. The tutorial assumes participants are familiar with the typed lambda calculus, operational semantics, basic typing rules, and type soundness proofs; those who are a bit rusty should still be able to follow along.