PAL, managing Projects

STELF, like Twelf, actually has an imperative running model for its logical declerations. Unlike Twelf, this is a completly new language, and not merely a integration into another language, and also is required to interact with it¹

The Mental Model

Each STELF program is not a description of a theory, but rather a sequence of commands that change the current state. Rather than thinking of a sequence like “nat is a sort, zero is a nat, succ is a function from nat to nat”, we instead think of “declare a sort nat, declare a term zero of nat, declare a term succ of nat to nat” To reference a theory is then to assure that the theory is in context. This imperative reading is the basis for the module system.

There are many benifits to this approach:

1. It leads to a natural system for writing literate files. Indeed, STELF files are literate by default (and you can’t change that).
2. It allows for a more natural way to think about extensions. You can read the program in the same way STELF does.
3. Macros!
4. It gives a simple way to embed a module system.

Footnotes

1. Unfourtanetly, all the naming time went to figuring out what the whole project should be called, so the languages are just called Outer and Inner. ↩