Date of Award

August 2017

Degree Type

Thesis

Degree Name

Master of Science

Department

Computer Science

First Advisor

John Boyland

Committee Members

Ethan V. Munson, Christine Cheng

Keywords

Education, LF, M2+, Proof Assistant, SASyLF, Unification

Abstract

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.

Download

Share

COinS