Coq

Coq

Coq هو مساعد إثبات ، والذي يسمح لك بكتابة بروفات رياضية بطريقة صارمة ورسمية ، وتأكد من صحتها بواسطة الكمبيوتر.
Coq هو مساعد إثبات ، والذي يسمح لك بكتابة بروفات رياضية بطريقة صارمة ورسمية ، وتأكد من صحتها بواسطة الكمبيوتر.كما يسمح البرمجة مع البراهين من صحة رمز ، وأنواع التابعة.

موقع الكتروني:

التصنيفات

بدائل Coq لجميع المنصات مع أي ترخيص

F*

F*

F * هي لغة برمجة وظيفية تشبه ML تهدف إلى التحقق من البرنامج.يمكن لـ F * التعبير عن مواصفات دقيقة للبرامج ، بما في ذلك خصائص الصحة الوظيفية.يمكن ترجمة البرامج المكتوبة باللغة F * إلى OCaml أو F # للتنفيذ.
Isabelle

Isabelle

إيزابيل مساعد إثبات لكتابة وفحص البراهين الرياضية عن طريق الكمبيوتر.
Agda

Agda

Agda هي لغة برمجة وظيفية مكتوبة بشكل صحيح.يحتوي على عائلات استقلالية ، أي أنواع البيانات التي تعتمد على القيم ، مثل نوع المتجهات ذات الطول المحدد.