MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 01-Dec-96 20:31:26 GMT
Content-Type: text/html
Content-Length: 2728
Last-Modified: Thursday, 01-Aug-96 17:12:28 GMT
PRL Seminar talks
PRL Seminars
Here are some of the slides for the talks I have given in the Nuprl
seminar. These slides can be pretty technical, and assume knowledge
of the Nuprl system and type theory. In some cases I
present information at an intuitive level that is technically imprecise.
All slides are in Portable Document Format (PDF). You can obtain a
PDF reader from Adobe for just about any machine you
can imagine using. I prepared these presentations using Adobe
Persuasion and Adobe Illustrator.
-
Modules February, 1996. This is
my most recent version of formal modules and objects.
-
Modules October, 1995. This
is an earlier version of formal modules.
-
Horus November, 1995. We
are performing a verification of the Horus group
communication system. These slides give an outline of the
verification process.
-
Types October, 1994. These
slides cover some new type additions I was proposing for Nuprl. This
includes very-dependent function types.
-
Square Root Verification
May, 1994. This talk is about the verification of a hardware square
root algorithm by program transformation. The slides don't contain
much explanation. The paper we wrote
for TPCD 1994
(Theorem Provers in Circuit Design) is a better resource.
-
Theories March, 1994. This
is a very early version of formal theories (modules) in Nuprl.
-
Majority Vote November,
1993. This is the first formalization I did in Nuprl. I gives some
idea of the problems I first encountered using Nuprl, and it provides
motivation for my current work in Nuprl.
Some other talks.
Horus talks
-
Horus Verification January, 1996. This
is a very high-level overview of the Horus verification effort.
-
Horus Verification April, 1996. Here
is a slightly more detailed, but still high-level, version of the Horus verification.