لغة Coq هي عبارة عن برنامج يستخدم كأداة للإثباتات التفاعلية في علم الحوسبة. تم إطلاقها لأول مرة في عام 1989، وهي توفر بيئة للتعبير عن التحقيقات الرياضية، وفحص الأدلة الميكانيكية لهذه التحقيقات، ومساعدة المستخدمين في إيجاد الأدلة الرسمية، واستخراج برامج معتمدة من الأدلة البنائية لمواصفاتها الرسمية.
يعمل Coq ضمن نظرية حساب البناء التكراري، وهي تفرع من حساب البناء. يجب التنويه إلى أن Coq ليست برنامجًا لإثبات النظريات تلقائيًا، ولكنها تتضمن تكتيكات لإثبات النظريات تلقائيًا وإجراءات قرارية متعددة.
من الجوائز التي حصلت عليها لغة Coq جائزة “جائزة نظام البرمجيات للعام 2013” من جمعية الحوسبة ACM، وقد منحت الجائزة لمجموعة من المطورين والمساهمين في المشروع، بما في ذلك Thierry Coquand، وGérard Pierre Huet، وChristine Paulin-Mohring، وغيرهم.
يمكنك العثور على مزيد من المعلومات حول لغة Coq في صفحتها على ويكيبيديا: Coq Wikipedia.
تجدر الإشارة إلى أن لغة Coq مفتوحة المصدر ويمكن الوصول إليها من خلال مستودعات الشفرة المركزية المتاحة عبر الإنترنت.