Skip to main content
PRL Project

Discussion of Methods of Sharing Formal Mathematics

by Evan Moran

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

Evan's "Real vs. Ideal" slide