Date of Award
Master of Science
Ethan V. Munson, Christine Cheng
Education, LF, M2+, Proof Assistant, SASyLF, Unification
SASyLF is an interactive proof assistant whose goal is to teach: about type systems,
language meta-theory, and writing proofs in general. This software tool stores user-specified
languages and logics in the dependently-typed LF, and its internal proof structure closely
resembles M2+ . This thesis describes a new usability feature of SASyLF, “where” clauses,
which make explicit previously hidden substitutions that arise through constructs in the proof
code, primarily case analyses. An overview of SASyLF and logical frameworks is given, with
motivating examples. The requirements for “where” clauses are discussed, including a formal
definition of correctness. The feature’s implementation in SASyLF is outlined, and future
extensions are discussed.
Ariotti, Michael David, "Making Substitutions Explicit in SASyLf" (2017). Theses and Dissertations. 1576.