Proving metatheorems with STELF

The 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.

This introduction assumes this story is somewhat familiar to you. If not, you should read a textbook such as TAPL or PFPL. The STELF version of the story goes something like this:

One day, a programming language designer has an idea.
She formalizes the syntax and judgements of the language in the LF logical framework.
She uses STELF to check her proofs of the theorems.
She uses STELF to run the language definition itself to try out some examples.
Her paper includes a STELF 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 tutorial pays a lot of attention to the question “how do I know that what I wrote down and proved on paper, and what I wrote down and proved in STELF, are exactly the same thing?” Checking that these two things are the same is called adequacy, and it’s an important problem whenever you’re using a theorem proving like STELF, Agda, or Rocq. But it definitely has the flavor of “checking lots of fiddly details,” and so it’s reasonable to skip discussions of adequacy in this tutorial if you’re exploring STELF for the first time.

First order representations: The natural numbers

The first layer of this introduction uses a very simple deductive system, the natural numbers with addition, to introduce the STELF methodology.

Higher-order representations: The simply-typed lambda calculus

The second layer tells the same story for a programming language with variable binding (the simply-typed lambda calculus), which is where STELF really shines.

Beyond the simply-typed lambda calculus

The third layer presents some more-interesting proofs and introduces one additional feature of STELF, the ability to do proofs about open terms.