In this section, we discuss the ways in which the logical features described from a mathematical standpoint in the previous section are implemented in Watson.

- The syntax of the term language of Watson
- Implementing algebraic logic in Watson
- Implementing case expression logic in Watson
- Implementing stratified abstraction in Watson
- The handling of variable binding: de Bruijn levels and the formal definition of substitution
- Abstraction and reduction by built-in tactics
- Examples of the implementation of abstraction in Watson
- The implementation of stratification in Watson: relative type and opacity
- Examples of the implementation of stratification
- Support for strongly cantorian domains
- Examples of the implementation of strongly cantorian domains
- Definitions in Watson
- Fine points of matching: limited higher order matching and commutative matching
- Special effects