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?
4
-
$\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$– Andrej BauerAug 5 at 9:35
-
$\begingroup$ @AndrejBauer Yes but they haven't responded yet. This is not a tragedy, i do it for fun. $\endgroup$– Pavel ShuhrayAug 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$– Andrej BauerAug 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$– Meven Lennon-BertrandAug 24 at 11:28
Add a comment
|