Нупрл
-
Обзор системы Nuprl
- Nuprl — это система для разработки доказательств, анализа и верификации программного обеспечения.
- Основана в 1980-х годах, поддерживается проектом PRL Корнеллского университета.
- Версия Nuprl 5 известна как FDL и включает графический интерфейс пользователя, веб-редактор и Emacs.
-
Дизайн и архитектура
- Использует систему типов Мартина-Лефа для моделирования математических утверждений.
- Включает различные редакторы и средства оценки, а также трансляторы для работы с инструкциями.
- Управляется с помощью ML, имеет распределенную открытую архитектуру и предназначена для веб-сервисов.
-
История и развитие
- Первый выпуск в 1984 году, подробное описание в 1986 году.
- Nuprl 2 стала первой версией Unix, Nuprl 3 предоставил машинное доказательство парадокса Жирара и леммы Хигмана.
- Nuprl 4 адаптирован для Всемирной паутины, Nuprl 5 предложен в 2000 году, а в 2002 году опубликовано справочное руководство.
-
Преемники и рекомендации
- JonPRL и RedPRL также основаны на теории вычислительных типов, RedPRL вдохновлена Nuprl.
- Ссылки на документацию и публикации разработчиков Nuprl доступны на веб-страницах проекта PRL и RedPRL.
Полный текст статьи: