Presentations

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.

Nuprl presentations

Here are some of the slides of presentations about Nuprl. These slides can be pretty technical, and assume knowledge of the Nuprl system and type theory.

• Formal Mathematics and Programming April, 1997. This is a longer and more technical talk about Nuprl-Light.

Prl Seminars

• Logical Programming Environments March, 1998. Nuprl-Light can be considered to be a logical programming environment: it enhances a programming language with a logic, and it enables the use of a variety of logical tools. I also discuss the application to Ensemble.
• Sharing Formal Mathematics and Programming February, 1997. This is a short talk giving an overview of my work on Nuprl-Light, and systems for sharing and relating formal logics and type theories.
• Nuprl tutorial February, 1997. An overview of the Nuprl system.
• Object Encodings November, 1996. This presents formal encoding of object-oriented programming in type theory.
• Nuprl-Light September 1996. This is an overview of the Nuprl-Light system.
• Formal Objects in Type Theory September 1996.
• 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.

Ensemble Jukebox

• Ensemble Jukebox: a Platform for Distributed Entertainment, December 1997, The Ensemble Jukebox, a digital audio server with emphasis on the architecture, the service, and security.

Ensemble Presentations

• Applying Formal Tools to Compositional Systems, August 1997, Another overview of the Ensemble optimization/verification.

Horus

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