Daniel Luick

In computer science there it is often useful to be able to prove that programs are correct in some way. One way we can prove this is by proving a property about the programming language as a whole. Proofs about programming languages as a whole, however, are difficult for a couple reasons. One is that they are conceptually difficult; it is difficult to think of how to prove something that hasn't been proven. However, these proofs also require dealing with formalizations that are tedious and error prone, and require careful bookkeeping. Proof assistants can take care of this bookkeeping aspect, freeing the scientist to focus on the conceptual difficulty. Proof assistants have three parts: a specification language with which to formalize the object language within the proof assistant, a logic to state properties of interest, and a tactics language to prove these properties. I have been working with Adelfa, a proof assistant being developed at the University of Minnesota. Adelfa uses a specification language called LF. Using Adelfa, I have formalized a language called the Simply Typed Lambda Calculus and used Adelfa to prove the STLC is type safe and to partially prove it is strongly normalizing, two properties which show programs based on the STLC are secure and terminating.