لین (دستیار اثبات)
نرم افزار اثبات تعاملی و خودکار قضایا / From Wikipedia, the free encyclopedia
Lean یک دستیار اثبات و یک زبان برنامهنویسی تابعی است.[1] این زبان مبتنی بر حساب سازهها با نوعهای القایی است. Lean یک پروژه متنباز است که بر روی گیتهاب میزبانی میشود. این زبان به طور اولیه توسط لئوناردو د مورا در حین اشتغال در مایکروسافت ریسرچ توسعه داده شد و اکنون در آمازون وب سرویسز ادامه دارد. توسعه این زبان در حال حاضر توسط سازمان Lean سازمان تحقیقات متمرکز (FRO) پشتیبانی میشود.
اطلاعات اجمالی پارادایم برنامهنویسی, توسعهدهنده ...
![]() | |
پارادایم برنامهنویسی | برنامهنویسی تابعی، برنامهنویسی دستوری |
---|---|
توسعهدهنده | Lean FRO |
ظهوریافته در | ۲۰۱۳؛ ۱۱ سال پیش (۲۰۱۳-خطا: زمان نامعتبر}}) |
انتشار پایدار | |
انتشار آزمایشی | |
ایستا، قوی، استنتاجی | |
زبان پیادهسازی | Lean , C++ |
سیستمعامل | چندسکویی |
پروانه | مجوز آپاچی ۲.۰ |
وبگاه | |
متأثر از | |
ML Coq هسکل |
بستن