PRL Seminars

We have currently built up large, monolithic bodies of formal mathematics and programming around the world, and we have no effective way of combining or relating them.

In this PRL seminar, I'll cover one of the techniques we can use to relate this knowledge: the formal module system. I'll give an informal introduction to the module system I have implemented in Nuprl-Light, and I'll discuss some of the general problems facing the module designer.

This is intended to be more of a tutorial than a formal justification, and the floor will remain open for questions.