Talks

Foundations for the Management of Formal Mathematical Knowledge.
Given by Robert L. Constable at the Small Types Workshop, Nijmegen November 2004.
A Graph-Based Approach towards Discerning Inherent Structures in a
Digital Library of Formal Mathematics.
Given by Lori Lorigo at the Mathematical Knowledge Management, Bialowieza, Poland, September 2004.
Services of the Formal Digital Library (FDL).
Given by Lori Lorigo at the Second North American Workshop on Mathematical Knowledge
Management, Phoenix, Arizona, January 2004.
Steps Toward a World Wide Digital Library of Formal Mathematics.
Keynote talk by Robert Constable at the Mathematical Knowledge Management
Symposium, Edinburgh, Scotland, November 2003.
Introduction to MetaPRL Theorem Prover.
Tutorial given by Jason Hickey, et al., at TPHOLs 2003, in Rome, Italy, September 2003.
Formalizing Abstract Algebra in Type Theory with Dependent Records.
Poster session given by Xin Yu at TPHOLs 2003, in Rome, Italy, September 2003.
MetaPRL -- A Modular Logical Environment.
Given by Jason Hickey at TPHOLs 2003, in Rome, Italy, September 2003.
Information Intensive Proof Technology.
A series of talks given by Robert Constable at the Marktoberdorf International Summer School, Proof Technology and Computation, August 2003.
      Lecture 1, Series Introduction and Type Theories
      Lecture 2, Set Theoretic Semantics for Type Theory
      Lecture 3, Relationships Between Sets and Types
      Lecture 4, Event Systems
Constructively Characterizing Fold and Unfold.
Given by Tjark Weber at LOPSTR 2003, in Uppsala, Sweden,
August 2003.
Formal Compiler Implementation in a Logical Framework.
Given by Jason Hickey at MERLIN 2003, in Uppsala, Sweden, August 2003.
Practical Reflection in Nuprl.
Given by Eli Barzilay at LICS '03, Ottawa, Canada, June 2003.
Formal Abstract Algebra in MetaPRL.
Given by Jason Hickey at City College of New York, May 2003.
An Interactive Digital Library of Algorithmic Knowledge.
Given by Lori Lorigo at the University of California, Berkeley, April 2003.
Building and Using a Library of Formal Mathematics.
Invited talk given by Robert Constable at Ben Gurion University, Beer Sheva, Israel,
January 2003.
Design of an Interactive Digital Library of Formal Algorithm Knowledge.
Given by Lori Lorigo at the Stanford University, December 2002.
Building and Using a Library of Formal Mathematics.
Invited talk given by Robert Constable at Reading, England, October 2002.
The Nuprl Proof Development System.
Given by Christoph Kreitz at the Calculemus Autumn School, Pisa, Italy,
September/October 2002.
Logical Foundations for Digital Libraries of Formal Mathematics.
Invited talk given by Robert Constable to the Association for Symbolic Logic, Muenster, Germany, August 2002.
Building an Interactive Library of Formal Algorithmic Knowledge.
Invited talk given by Robert Constable at NA-MKM, McMaster University, Hamilton, Ontario, June 2002.
Designing Reliable, High-Performance Networks with the Nuprl Logical Programming Environment. Given by Christoph Kreitz at the AAAI Spring Symposium on Logic Based Program Synthesis, Stanford University, Stanford, California, March 2002.
Formal Logical Environments for Building Reliable, High-Performance Software.
Given by Christoph Kreitz at Harvey Mudd College, Claremont, California, March 2002.
Logical Aspects of Digital Mathematics Libraries.
Given by Jim Caldwell at the First International Workshop on Mathematical Knowledge Management, Schloss Hagenberg, September 2001.
Designing Reliable, High-Performance Networks with the Nuprl Proof Development System. Given by Christoph Kreitz at the Dagstuhl workshop, "Dependent Type Theory Meets Practical Programming," Schloss Dagstuhl, Germany, August 2001.
Building Interactive Libraries of Formal Algorithmic Knowledge. Given by Robert Constable at the MURI Kickoff Meeting, Arlington, Virginia, July 2001.