Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
Abstract elided by the publisher.
Related papers
- Teaching algorithms and data structures with a proof assistant (invited talk) CPP 2021
- Lambda, the ultimate TA: using a proof assistant to teach programming language foundations ICFP 2009
- The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math" CPP 2011
- Live Verification in an Interactive Proof Assistant PLDI 2024
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant POPL 2006
- Separation logic for sequential programs (functional pearl) ICFP 2020
- TacTok: semantics-aware proof synthesis OOPSLA 2020
- Semantic cut elimination for the logic of bunched implications, formalized in Coq CPP 2022