Evolution of SASyLF 2008-2021
John Tang Boyland (University of Wisconsin-Milwaukee)
TL;DR
This paper chronicles the development and enhancements of SASyLF from 2008 to 2021, highlighting its sustained educational use and technical improvements like explicit substitutions and IDE support.
Contribution
It details the evolution of SASyLF, including new features such as explicit substitutions, logical connectives support, and IDE integration, maintaining its educational utility.
Findings
SASyLF has been continuously used in university courses since 2008.
Major enhancements include explicit substitutions and support for logical connectives.
IDE support has improved user experience and usability.
Abstract
SASyLF was released in 2008 and used as a proof assistant in courses at several universities. It proved itself useful and has continued to be used, and each iteration of use has encouraged further development: fixing bugs and adding enhancements. This paper describes how SASyLF was developed while keeping true to its purpose. Most notable are making substitutions explicit, support of "and" and "or," support for mutual and lexicographic induction, and IDE support.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.