Agda

Agda

Agda هي لغة برمجة وظيفية مكتوبة بشكل صحيح.يحتوي على عائلات استقلالية ، أي أنواع البيانات التي تعتمد على القيم ، مثل نوع المتجهات ذات الطول المحدد.
Agda هي لغة برمجة وظيفية مكتوبة بشكل صحيح.يحتوي على عائلات استقلالية ، أي أنواع البيانات التي تعتمد على القيم ، مثل نوع المتجهات ذات الطول المحدد.كما أن لديها وحدات نمطية ، مشغلات mixfix ، أحرف Unicode ، واجهة Emacs التفاعلية التي يمكن أن تساعد المبرمج في كتابة البرنامج.اغدا هو مساعد إثبات.إنه نظام تفاعلي للكتابة والتحقق من البراهين.يعتمد Agda على نظرية النوع البديهية ، وهو نظام تأسيسي للرياضيات البنائية التي طورها السويدي بير مارتين لوف.لديها العديد من أوجه التشابه مع مساعدي إثبات آخرين بناءً على أنواع تابعة ، مثل Coq و Epigram و Matita و NuPRL.
agda

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

Coq

Coq

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

F*

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

Isabelle

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