Mathématiques assistées par ordinateur
avec Benedikt

Comme le typage dépendant ne marche pas trop bien, on veut le simuler dans un cadre qui marche bien, comme HOL. Autrement dit on veut voir COC comme un formalisme qu'on va compiler en HOL.