Habilitation à Diriger des Recherches

Un exemple:

Séquent: définit une propriété d'un certain sujet

         env |- exp : type 

Jugement: déclare le type d'un séquent

      Judgement ENV |- EXP : TYPE 

Règle: permet de déduire de nouveaux faits

      e |- Var : T    e |- Exp : T
      ----------------------------
           e |- Var := Exp ;