Modes of use

STELF is a very flexible system that lends itself to a wide variety of deductive systems. This flexibility can be confusing, as different uses of STELF look very different from one another. Here, we attempt to describe a number of the major modes of use of STELF.

• A framework for defining logics - The judgments of a logic are encoded in STELF so that STELF’s type checker can check the correctness of proofs. The Foundational Proof Carrying Code project at Princeton used this method extensively to write proofs about programs that could be verified by a small, trusted checker. The primary tutorial for this style is Andrew Appel’s [http://www.cs.princeton.edu/~appel/twelf-tutorial/ Hints on Proving Theorems in STELF]
• **Proving properties about deductive systems - This is a relatively recent use of STELF, but it is also perhaps the most widespread. The judgments of a deductive system, typically a programming language, are encoded in STELF, and then STELF is used to verify metatheorems about that deductive system. The primary tutorial for this style is Dan Licata’s Proving metatheorems with STELF, though several others can be found on the Documentation page.
• Typed logic programming - STELF can also be used as an advanced typed logic programming language, a variant of Lambda Prolog with dependent types.

Most large projects integrate several of these modes of use. There are some limitations to this integration, particularly in that the constraint domains and type level definitions cannot be used in projects that want to prove metatheorems.

A framework for defining logics

The “theorem style” use of STELF described in Andrew Appel’s notes defines a deductive system, typically a logic: first a set of propositions (propositions often have type o for historical reasons), and then axioms about how propositions can be proven. Appel’s FPCC project uses higher-order logic, but here we define a much simpler propositional logic.

%sort o %.
% Propositions
%term true o %.
%term imp %pi o %-> o %-> o %.
%prec %right 10 imp %.
%term and %pi o %-> o %-> o %.
%prec %right 11 and %.
% Judgments
%sort pf {_ o} %.
%term true-i pf true %.
%term imp-i %pi (%pi (pf A) %-> (pf B)) %-> (pf (A imp B)) %.
%term imp-e %pi (pf (A imp B)) %-> (pf A) %-> (pf B) %.
%term and-i %pi (pf A) %-> (pf B) %-> (pf (A and B)) %.
%term and-e1 %pi (pf (A and B)) %-> (pf A) %.
%term and-e2 %pi (pf (A and B)) %-> (pf B) %.

Having defined this a logic, the point of the exercise is to write out proofs by hand (perhaps with the assistance of tactical theorem proving). These proofs can then be automatically verified by STELF, or by an extremely small independent checker.

Here are some examples from the first lecture of Hints on Proving Theorems in STELF:

%define symm-and (%pi (pf (A and B)) %-> (pf (B and A))) [p1 pf (A and B)] and-i (and-e2 p1) (and-e1 p1) %.
%define and-l (%pi (pf (A and B)) %-> (%pi (pf A) %-> (pf B) %-> (pf C)) %-> (pf C)) [p1 pf (A and B)] [p2 %pi (pf A) %-> (pf B) %-> (pf C)] imp-e (imp-e (imp-i ([p3] imp-i (p2 p3))) (and-e1 p1)) (and-e2 p1) %.
%define example-abc (%pi (pf (A and B)) %-> (pf C) %-> (pf (B and C and (A and C)))) [p1 pf (A and B)] [p2 pf C] and-l p1 ([p3 pf A] [p4 pf B] and-i (and-i p4 p2) (and-i p3 p2)) %.

Even this logic allows us to prove a number of interesting theorems; the definition of a more complex logic (without much commentary) can be found at Zermelo Frankel.

Proving properties about deductive systems

The “metatheorem style” use of STELF defines a deductive system, typically a programming language: first the abstract syntax of the language, and then the static and dynamic semantics. Here is an example of a simple lambda calculus with product types (we don’t define the dynamic semantics here, see Representing the judgements of the STLC for a similar example).

%sort exp %.
%sort tp %.
% Expressions
%term exp/unit exp %.
%term exp/lam %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term exp/app %pi exp %-> exp %-> exp %.
%term exp/pair %pi exp %-> exp %-> exp %.
%term exp/fst %pi exp %-> exp %.
%term exp/snd %pi exp %-> exp %.
% Types
%term unit tp %.
%term arrow %pi tp %-> tp %-> tp %.
%prec %right 10 arrow %.
%term pair %pi tp %-> tp %-> tp %.
%prec %right 11 pair %.
% Static semantics
%sort of {_ exp} {_ tp} %.
%term of/unit of exp/unit unit %.
%term of/lam
  %pi (of (exp/lam T1 ([x] E x)) (T1 arrow T2))
  %<- ({x exp} %pi (of x T1) %-> (of (E x) T2)) %.
%term of/app %pi (of (exp/app E E') T) %<- (of E' T') %<- (of E (T' arrow T)) %.
%term of/pair %pi (of (exp/pair E1 E2) (T1 pair T2)) %<- (of E2 T2) %<- (of E1 T1) %.
%term of/fst %pi (of (exp/fst E) T1) %<- (of E (T1 pair T2)) %.
%term of/snd %pi (of (exp/snd E) T2) %<- (of E (T1 pair T2)) %.
% Dynamic semantics
%sort step {_ exp} {_ exp} %.
% ... and so on

Having defined this programming language, we are generally interested in proving metatheorems relating that programming language to a particular dynamic semantics - showing, for instance, that a certain evaluation strategy will preserve the type of the terms it evaluates, and that if a closed can be given a type, it can either be reduced or it is already a value. We also may be interested in using the logic programming engine of STELF to run our typing judgments as a logic program, giving our language a reference type checker.

Discussion