PRL Seminars
Discussion of Methods of Sharing Formal Mathematics
Abstract
Evan Moran will say a few more words about his
work relating type theory and set theory. He will
mention applications of his work in showing the
compatibility of PVS type theory and Classical
Computational Type Theory.
We will use Evan's results as the basis for a discussion
of the value of hybrid proofs, the means of sharing
formal mathematics among theorem provers, and the
requirements for accounting mechanisms in the FDL
| 