PRL Seminars

Jason, Stuart, Rich Eaton and I will lead a discussion of the issues we have raised over the past two weeks concerning the design of a library of mathematical knowledge. I will present a specific example of two small theories that we want to store in a library and relate. We will see how to connect them semantically (using quotient types) and we will discuss how to compare them if we did not have this kind of semantics but relied on "sentinels" a la Stuart. Jason will discuss how he could implement sentinels in Nuprl-Light.

We plan to end with "three views of authentication in logic libraries". Here three different opinions will be aired and illustrated by our experience in trying to use Nuprl in a secure way.