Proving metatheorems with Twelf

From The Twelf Project
Jump to: navigation, search

Is this introduction for you?

The life story of a typical deductive system goes something like this: One day, a programming language designer has an idea for a new programming language. She writes down the language's abstract syntax. Then, she gives the syntax meaning by defining some judgements for it, such as a type system or an operational semantics. Next, she investigates the language's properties by proving some theorems. Maybe she fiddles with the language some to make the desired theorems true; maybe the idea doesn't work at all and she goes on to something else. Maybe she implements the language to try out some examples. Eventually, if the idea works out, she writes up a paper about the language. If it's a good idea, then she, or maybe someone who read the paper, will someday want to extend the language, or incorporate the idea into another language.

Twelf is a tool that assists people designing deductive systems: One day, a programming language designer has an idea. Then, she formalizes the syntax and judgements of the language in the LF logical framework. She uses Twelf to check her proofs of the theorems. She uses Twelf to run the language definition itself to try out some examples. Her paper includes a Twelf appendix, which makes her and her readers much more confident that the theorems in the paper are actually true. When someone goes to extend the language, he has a formal, machine-checkable artifact that he can study or perhaps even reuse directly.

This introduction assumes that the first version of this story is somewhat familiar to you (if not, you should read a textbook such as TAPL or PFPL). Here, you will learn the fundamentals of the Twelf version of the story. This guide unveils Twelf in several layers. The first layer uses a very simple deductive system (natural numbers with addition) to introduce the Twelf methodology. The second layer tells the same story for a programming language with variable binding (the simply-typed lambda calculus), which is where Twelf really shines. The third layer presents some more-interesting proofs and introduces one additional feature of Twelf, the ability to do proofs about open terms.

Table of contents

  1. First-order representations: The natural numbers
    1. Representing syntax
    2. Simply typed LF
    3. Representing judgements
    4. Full LF
    5. Proving totality assertions
    6. Proving metatheorems
    7. Summary (Answers to exercises)
  2. Higher-order representations: The STLC
    1. Representing syntax
    2. Representing judgements
    3. Proving metatheorems
    4. Proving totality assertions in non-empty contexts
    5. Proving metatheorems in non-empty contexts
    6. Summary (Answers to exercises)