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?

  • $\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 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 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 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 at 11:28


Your Answer

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

Browse other questions tagged or ask your own question.