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 de software. Desarrollado originalmente en la década de 1980 por Robert Lee Constable y otros, el sistema ahora es mantenido por el Proyecto PRL en la Universidad de Cornell . La versión actualmente admitida, Nuprl 5, también se conoce como FDL (Biblioteca digital formal). Nuprl funciona como un sistema automatizado de prueba de teoremas y también se puede utilizar para proporcionar asistencia para la prueba .
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 en las declaraciones de 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 contactar la dirección de correo electrónico proporcionada en la página web del Sistema Nuprl. [2]
Nuprl se publicó 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ó una prueba de máquina 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 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 de 2000 . En 2002 se publicó un manual de referencia para Nuprl 5. [5] Nuprl ha sido objeto de muchas publicaciones sobre ciencias de la computación .
Tanto el sistema JonPRL como el RedPRL también se basan en la teoría de tipos computacionales. [6] RedPRL está explícitamente "inspirado por Nuprl". [7]