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 ...