This meaning theory follows the Wittgensteinian meaning-as-use tradition. The meaning is based on rules for building objects (introduction rules) of types and computation rules (elimination rules) for computing with these objects. A difference from much of the Wittgensteinian tradition is that also higher order types like \(\N \rightarrow \N\) are given meaning using rules.