This program is tentative and subject to change.

Mon 16 Jan 2023 14:00 - 15:30 at Park - Tutorials 6A
Mon 16 Jan 2023 16:00 - 17:30 at Park - Tutorials 6B

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 http://www.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.

This program is tentative and subject to change.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:30
Tutorials 6ATutorialFest at Park
14:00
90m
Tutorial
Using a Proof Assistant to Teach PL Theory, Without the Overhead
TutorialFest
Jonathan Aldrich Carnegie Mellon University, John Boyland Univeristy of Wisconsin, Milwaukee
16:00 - 17:30
Tutorials 6BTutorialFest at Park
16:00
90m
Tutorial
Using a Proof Assistant to Teach PL Theory, Without the Overhead
TutorialFest
Jonathan Aldrich Carnegie Mellon University, John Boyland Univeristy of Wisconsin, Milwaukee