Odersky presents a new method for specifying static semantics. Contextual constraints (such as type checking) are specified using formulas from the first-order predicate calculus, while reasoning about the set of nodes in the program’s derivation tree. The new notation is thus called CADET (calculus on derivation trees).

Like many other methods, CADET is used to specify static semantics by imposing restrictions on the derivation tree. Unlike most other methods, CADET does not seem to need the “auxiliary” tools (data structures or mappings) that are conventionally used to transport data from one place to another in the tree. Instead, CADET is used to reason about such nodes directly. The author says CADET has been used successfully in the specification of the language Oberon.

The paper is well written, and the main thesis (that CADET offers a more abstract, less implementation-oriented alternative) is presented well. CADET is compared directly against a number of other methods, including attribute grammars, functional methods, logic-based methods, Axiomatic Denotational Language (ADL), and constructive theories.

Overall, this paper is a well-formulated contribution to the state of the art. As with most other specification methods of programming languages, however, CADET faces long odds against gaining general acceptance. Specifically, a method for generating translators automatically from CADET specifications is needed before the technique can be considered practical.