A Typol program consists of a list of global declarations (judgements, import clauses, definitions) and a set, or sets, of rules which may be either inference rules or axioms. These rules explain how to deduce sequents from other sequents.
Inference rules have the following form: Typol semantics state that when we have proved all of the premises, we have proved the conclusion and thus the rule. The numerator is a list of sequents, the conclusion a single sequent, and the subject of the conclusion is called the subject of the rule. The inference rule:
may be interpreted as follows:
The value of the tree (whose associated operator is plus) with descendents and is where is the result of the evaluation of , is the result of the evaluation of , and is the result of the addition of and .
This rule has three premises, two of which are recursive calls to evaluate the descendents of the subject tree, and the third actually adds the resulting integers. The subject of this rule is the pattern .
Axioms are rules without premises and therefore serve to stop recursive deduction. In Exp, we use the axiom:
which may be interpreted as The value of the integer N is itself. The word integer that appears in the axiom and previous inference rule is the name of the atomic operator in the abstract syntax.