PRL Seminars

Doug is willing to talk to us about his results importing HOL theorems into Nuprl and the prospects for doing the same kind of thing for PVS.

We have a joint DARPA research grant with Doug on topics that include learning how to share mathematics with other systems. Doug has demonstrated that it is cheaper to build connections to other provers than to reprove many basic results. He has been discussing with us some of the issues that arise in sharing results with PVS.