Summary and exercises

This page is part of the introduction to proving metatheorems with STELF.

Take-aways

The lessons you should take from this section are:

• LF’s binding structure enables elegant representations of object-language binding and hypothetical judgements.
• World declarations permit totality assertions about type families in non-empty contexts.
• 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 STELF. You’ve seen all of the basic machinery that STELF 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 STELF.

Test yourself

Here are a few suggestions for additional explorations:

Adding features to the simply-typed lambda calculus

A standard extension of the simply-typed lambda calculus is pairs:

$${ \Gamma \vdash e_1 : \tau_1 \qquad \Gamma \vdash e_2 : \tau_2 \over \Gamma \vdash \langle e_1, e_2 \rangle : \tau_1 \times \tau_2 }\mathit{of\textit{-}pair}$$ $${ \Gamma \vdash e : \tau_1 \times \tau_2 \over \Gamma \vdash \pi_1\,e : \tau_1 }\mathit{of\textit{-}proj_1} \qquad { \Gamma \vdash e : \tau_1 \times \tau_2 \over \Gamma \vdash \pi_2\,e : \tau_1 }\mathit{of\textit{-}proj_2}$$

The dynamic semantics of pairs have a number of rules, but they are all relatively straightforward:

$${ e_1 \, \mathtt{value} \qquad e_2 \, \mathtt{value} \over \langle e_1, e_2 \rangle \, \mathtt{value} }\mathit{value\textit{-}pair}$$ $${ e_1 \mapsto e_1' \over \langle e_1 , e_2 \rangle \mapsto \langle e_1', e_2 \rangle }\mathit{step\textit{-}pair_1} \qquad { e_1 \, \mathtt{value} \qquad e_2 \mapsto e_2' \over \langle e_1 , e_2 \rangle \mapsto \langle e_1, e_2' \rangle }\mathit{step\textit{-}pair_2}$$ $${ e \mapsto e' \over \pi_1 \, e \mapsto \pi_1 \, e' }\mathit{step\textit{-}proj_1} \qquad { e \mapsto e' \over \pi_2\, e \mapsto \pi_2 \, e' }\mathit{step\textit{-}proj_2}$$ $${ e_1 \, \mathtt{value} \qquad e_2 \, \mathtt{value} \over \pi_1 \, \langle e_1 , e_2 \rangle \mapsto e_1 }\mathit{step\textit{-}proj\textit{-}beta_1} \qquad { e_1 \, \mathtt{value} \qquad e_2 \, \mathtt{value} \over \pi_2 \, \langle e_1 , e_2 \rangle \mapsto e_2 }\mathit{step\textit{-}proj\textit{-}beta_2}$$

Add these to your formalization of the simply-typed lambda calculus and extend the proof of preservation to cover this new type.

Next steps

You now have everything you need to start proving metatheorems with STELF! The proof techniques covered in the tutorials are likely to be valuable as you continue. If you’re interested in proving progress for the simply typed lambda calculus formulation, you’ll do well to start by learning about output factoring.