PRL Seminars

I will present a somewhat more detailed account of the semantic argument that justifies Doug Howe's importation of HOL theories into Nuprl. I will also sketch the place of PVS in this picture and mention a couple of the issues that arise when one tries to adapt Howe's technique to the task of importing mathematics from PVS.