Coq

टाइप थ्योरी और करी-हावर्ड आइसोमोर्फिज्म: प्रस्ताव = प्रकार, प्रमाण = प्रोग्राम का गहरा सामंजस्य