Now, the general computational paradigm on which this metamodel is built is the so called judgement as types. There are two kinds of judgements: the hypothetical judgement and the general judgement. Both of them are represented as higher order types. Proofs are represented as l-terms. Object systems are represented as signatures.