stringtranslate.com

Нупрл

Nuprl — это система разработки доказательств, обеспечивающая компьютерный анализ и доказательства формальных математических утверждений, а также инструменты для проверки и оптимизации программного обеспечения. Первоначально разработанная в 1980-х годах Робертом Ли Констеблем и другими, система в настоящее время поддерживается проектом PRL в Корнелльском университете . Текущая поддерживаемая версия, Nuprl 5, также известна как FDL (Formal Digital Library). Nuprl функционирует как автоматизированная система доказательства теорем и может также использоваться для оказания помощи в доказательстве .

Дизайн

Nuprl использует систему типов, основанную на интуиционистской теории типов Мартина-Лёфа , для моделирования математических утверждений в цифровой библиотеке . Математические теории могут быть построены и проанализированы с помощью различных редакторов, включая графический пользовательский интерфейс , веб-редактор и режим Emacs . Различные оценщики и механизмы вывода могут работать с утверждениями в библиотеке. Трансляторы также позволяют манипулировать утверждениями с помощью программ Java и OCaml . [1] Вся система управляется с помощью варианта ML .

Архитектура Nuprl 5 описывается как «распределенная открытая архитектура » [1] и предназначена в первую очередь для использования в качестве веб-сервиса, а не как отдельного программного обеспечения. Те, кто заинтересован в использовании веб-сервиса или переносе теорий из старых версий Nuprl, могут связаться по адресу электронной почты, указанному на веб-странице Nuprl System. [2]

История

Nuprl был впервые выпущен в 1984 году и впервые был подробно описан в книге «Реализация математики с помощью системы разработки доказательств Nuprl» [3] , опубликованной в 1986 году. Nuprl 2 была первой версией Unix . Nuprl 3 обеспечивала машинное доказательство для математических задач, связанных с парадоксом Жирара и леммой Хигмана . Nuprl 4, первая версия, разработанная для Всемирной паутины , использовалась для проверки протоколов когерентности кэша и других компьютерных систем. [4]

Текущая архитектура системы, реализованная в Nuprl 5, была впервые предложена в докладе конференции 2000 года . Справочное руководство по Nuprl 5 было опубликовано в 2002 году. [5] Nuprl был предметом многих публикаций по информатике .

Преемники

Обе системы JonPRL и RedPRL также основаны на теории вычислительных типов. [6] RedPRL явно «вдохновлен Nuprl». [7]

Ссылки

  1. ^ ab "Распределенная открытая архитектура Nuprl 5". Проект PRL . Получено 7 марта 2015 г.
  2. ^ "Nuprl System". Проект PRL . Получено 7 марта 2015 г.
  3. ^ Констебль, Роберт и др. (1986). Реализация математики с помощью системы разработки доказательств Nuprl. Энглвуд Клиффс, Нью-Джерси: Prentice-Hall. ISBN 1468059106. Получено 7 марта 2015 г.
  4. ^ Аллен, Стюарт; Констебль, Роберт; Итон, Ричард; Крейц, Кристоф; Лориго, Лори. "Открытая логическая среда Nuprl (презентация слайдов 2000 года)" (PDF) . Получено 7 марта 2015 г.
  5. ^ Крайц, Кристоф (2002). Система разработки доказательств Nuprl, версия 5: справочное руководство и руководство пользователя (PDF) .
  6. ^ Харпер, Роберт; Ангиули, Карло (10 мая 2017 г.). «Вычислительная теория многомерных типов» (PDF) . 43-й симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования (POPL) .
  7. ^ "Логика народной утонченности". www.redprl.org . Получено 24.10.2017 .

Внешние ссылки