5
$\begingroup$

I want to use extensional type theory. I have installed Nuprl (on a virtual machine). It starts over an hour and I can't find examples or forums. Is there a better way?

$\endgroup$
5
  • 1
    $\begingroup$ Have you contacted the NuPRL people and asked for access to their instantiation of the system, as per nuprl.org/html/NuprlSystem.html? I think that's the preferred method of use. $\endgroup$ Aug 5, 2023 at 9:35
  • $\begingroup$ @AndrejBauer Yes but they haven't responded yet. This is not a tragedy, i do it for fun. $\endgroup$ Aug 7, 2023 at 16:50
  • $\begingroup$ Perhaps the project isn't so alive anymore? I haven't had much success getting a reaction from them a couple of years ago. Is anyone from NuPRL team listening? $\endgroup$ Aug 7, 2023 at 17:05
  • $\begingroup$ Depending on what you want to do, you might try and use the re-implementation of NuPRL's type theory in Coq: github.com/vrahli/NuprlInCoq. This should let you play with NuPRL's ETT in a theorem prover, although the interactivity and tooling will probably be subpar compared to using NuPRL itself. $\endgroup$ Aug 24, 2023 at 11:28
  • $\begingroup$ Not an answer, but I think both F* and Cedille are extensional type theories, so that might be where to look for non-nuprl extensional type theories $\endgroup$ Dec 23, 2023 at 3:43

1 Answer 1

6
$\begingroup$

... someone pointed me to this question a few days ago ...

The Nuprl group has ceased to exist about two years ago when Richard Eaton (the lead programmer) died unexpectedly and Bob Constable retired. The web pages at Nuprl.org contain plenty of information about the system, but as of now the domain doesn't seem to be linked the the servers at Cornell University anymore. I have asked the people at Cornell to reestablish that domain again but that may take a while.

Unlike Coq, Isabelle, and most other proof assistant Nuprl is not intended to be run standalone. It runs as a centralized database of formally verified mathematics that collects everything that has been done with the system. You're supposed to access the gateway at Cornell to work with the system. For now, unfortunately this is not an option, so you have to run the system that you have in your VM. It does take a long time to start the system because the entire database is checked. You're not supposed to shut it down afterwards. Just suspend the VM and resume it when you want to continue your work. I do that when I want to demonstrate the system in class.

On the long run we intend to set up an instantiation of the Nuprl system and the web site at the University of Potsdam in Germany. I have a copy of the entire system (and the web site) but it takes a lot of time to set everything up again since there is nobody I can ask about the implementation. Please be patient .. the system will be revived again some day.

Until then ... what is it that you want to do with the system? Maybe I can give you a few hints. Which version of the system did you install? The manual from 2000 is good for versions until about 2015. There were changes in the interaction with the system afterwards and there is not a lot of documentation about these.

I am not a regular member of this forum so please send email to me directly ([email protected])

$\endgroup$
2
  • 1
    $\begingroup$ It would be extremely valuable if NuPRL does not disappear. Is there any chance the system could be opened up and made available, so that it can get replicated and archived by several parties? $\endgroup$ Dec 23, 2023 at 15:01
  • 1
    $\begingroup$ I'll make the system available as soon as I get it to run properly. That may take some time, though. $\endgroup$ Dec 26, 2023 at 20:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.