Proving metatheorems:Summary: the STLC

From The Twelf Project
Jump to: navigation, search
Previous:
Proving metatheorems in non-empty contexts
Proving metatheorems with Twelf


Take-aways

The lessons you should take from this section are:

  1. LF's binding structure enables elegant representations of object-language binding and hypothetical judgements.
  2. World declarations permit totality assertions about type families in non-empty contexts.
  3. Such totality assertions can be used to prove general metatheorems about object-language entities that are represented using higher-order LF encodings.

What's next?

Now that you've made it through this introduction, you have the basic tools you need to start proving metatheorems with Twelf. You've seen all of the basic machinery that Twelf provides, and you are in a good position to understand the other documentation on this wiki. Your next step should be to read some of the tutorials, which describe clever modes of use of the techniques we have talked about here, or to read some of the case studies, which describe interesting applications of Twelf.

Test yourself

This section is under development; if you try other examples at this point, please add them here.

Before going on to the next section, you may wish to test yourself with the following exercises. Then see the answers.

  1. Add product types () to the STLC and extend the proof of preservation to cover this new type.
  2. Add your exercises here!


Previous:
Proving metatheorems in non-empty contexts
Proving metatheorems with Twelf