[Tutorial Fest @ POPL'23] Using a Proof Assistant to Teach PL Theory, Without the 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 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.
Видео [Tutorial Fest @ POPL'23] Using a Proof Assistant to Teach PL Theory, Without the Overhead канала ACM SIGPLAN
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 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.
Видео [Tutorial Fest @ POPL'23] Using a Proof Assistant to Teach PL Theory, Without the Overhead канала ACM SIGPLAN
Показать
Комментарии отсутствуют
Информация о видео
Другие видео канала
TyDe 2021 - Interactive Haskell Type Inference Exploration (Extended Abstract)[OCaml'22] Efficient “out of heap” pointers for multicore OCaml[PriSC'22] Composing Secure CompilersWarping Cache Simulation of Polyhedral Programs[SLE] Property-Based Testing: Climbing the Stairway to Verification[ML'22] Efficient and Scalable Parallel Functional Programming Through Disentanglement[CPP'23] CompCert: a journey through the landscape of mechanized semantics for verified co...Low-Latency, High-Throughput Garbage CollectionDISTAL: The Distributed Tensor Algebra CompilerIRDL: An IR Definition Language for SSA CompilersEfficient Compilation of Algebraic Effect Handlers[ICFP'22] Safe Couplings: Coupled Refinement TypesWebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration[ICFP'22] Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structu…Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation LogicInterval Universal Approximation for Neural Networks (Teaser)[POPL'22] Layered and Object-Based Game Semantics[POPL'22] Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites[VMCAI'22] Making PROGRESS in Property Directed ReachabilityPrinciples and Patterns of JastAdd-Style Reference Attribute GrammarsNatural Language-Guided Programming