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 .
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]
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 .
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]