stringtranslate.com

nuprl

Nuprl es un sistema de desarrollo de pruebas que proporciona análisis y pruebas por computadora de enunciados matemáticos formales, y herramientas para la verificación y optimización del software. Desarrollado originalmente en la década de 1980 por Robert Lee Constable y otros, el sistema ahora lo mantiene el Proyecto PRL de la Universidad de Cornell . La versión actualmente compatible, Nuprl 5, también se conoce como FDL (Biblioteca digital formal). Nuprl funciona como un sistema automatizado de demostración de teoremas y también se puede utilizar para proporcionar asistencia en la demostración .

Diseño

Nuprl utiliza un sistema de tipos basado en la teoría de tipos intuicionista de Martin-Löf para modelar enunciados matemáticos en una biblioteca digital . Las teorías matemáticas se pueden construir y analizar con una variedad de editores, incluida una interfaz gráfica de usuario , un editor basado en web y un modo Emacs . Una variedad de evaluadores y motores de inferencia pueden operar con las declaraciones en la biblioteca. Los traductores también permiten manipular declaraciones con programas Java y OCaml . [1] El sistema general se controla con una variante de ML .

La arquitectura de Nuprl 5 se describe como " arquitectura abierta distribuida " [1] y está destinada principalmente a ser utilizada como un servicio web en lugar de como software independiente. Aquellos interesados ​​en utilizar el servicio web o migrar teorías de versiones anteriores de Nuprl, pueden comunicarse con la dirección de correo electrónico proporcionada en la página web del Sistema Nuprl. [2]

Historia

Nuprl se lanzó por primera vez en 1984 y se describió por primera vez en detalle en el libro Implementing Mathematics with the Nuprl Proof Development System , [3] publicado en 1986. Nuprl 2 fue la primera versión de Unix . Nuprl 3 proporcionó pruebas mecánicas para problemas matemáticos relacionados con la paradoja de Girard y el lema de Higman . Nuprl 4, la primera versión desarrollada para la World Wide Web , se utilizó para verificar los protocolos de coherencia de caché y otros sistemas informáticos. [4]

La arquitectura del sistema actual, implementada en Nuprl 5, se propuso por primera vez en un documento de conferencia del año 2000 . En 2002 se publicó un manual de referencia para Nuprl 5. [5] Nuprl ha sido objeto de muchas publicaciones de informática .

Sucesores

Tanto el sistema JonPRL como el RedPRL también se basan en la teoría de tipos computacionales. [6] RedPRL está explícitamente "inspirada en Nuprl". [7]

Referencias

  1. ^ ab "Arquitectura abierta distribuida Nuprl 5". Proyecto PRL . Consultado el 7 de marzo de 2015 .
  2. ^ "Sistema nupcial". Proyecto PRL . Consultado el 7 de marzo de 2015 .
  3. ^ Alguacil, Robert; et al. (1986). Implementación de matemáticas con el sistema de desarrollo Nuprl Proof. Englewood Cliffs, Nueva Jersey: Prentice-Hall. ISBN 1468059106. Consultado el 7 de marzo de 2015 .
  4. ^ Allen, Estuardo; Alguacil, Robert; Eaton, Richard; Kreitz, Christoph; Lorigo, Lori. "El entorno lógico abierto de Nuprl (presentación de diapositivas de 2000)" (PDF) . Consultado el 7 de marzo de 2015 .
  5. ^ Kreitz, Christoph (2002). El sistema de desarrollo Nuprl Proof, versión 5: manual de referencia y guía del usuario (PDF) .
  6. ^ Harper, Robert; Angiuli, Carlo (10 de mayo de 2017). "Teoría computacional de tipos de dimensiones superiores" (PDF) . 43º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación (POPL) .
  7. ^ "La lógica del refinamiento del pueblo". www.redprl.org . Consultado el 24 de octubre de 2017 .

enlaces externos