Discussion of Issues in Logic Library Design

by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
1996-1997

Abstract
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.

Discussion of Issues in Logic Library Design

by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton 1996-1997

by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
1996-1997