Une formalisation des faisceaux et des schémas affines en théorie des types avec Coq. - Laurent Chicli (JFLA, 2001)

Mathematical Quotients and Quotient Types in Coq. - Laurent Chicli; Loic Pottier; Carlos Simpson (TYPES, 2002)