KnowledgeBase » 
SEMINAR
» ID = 624
Discussion of Methods of Sharing Formal Mathematics
by Evan Moran
2003-2004
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
