TPHOLs'99: 12th International Conference

Theorem Proving in Higher Order Logics: Emerging Trends

Certification of Sorting Algorithms in the Coq System

Jean-Christophe Filliātre and Nicolas Magaud

 

Implementing Extensible Theorem Provers

Kathi Fisler, Srhiram Krishnamurthi and Kathy Gray

 

A case study in class library verification: Java's vector class

Marieke Huisman, Bart Jacobs and Joachim Van Den Berg

 

Importing Isabelle Formal Mathematics into NuPRL

Pavel Naumov

 

Working with Linear Logic in Coq

James Power and Caroline Webster

 

Embedding Algebraic Specifications in HOL

Dan Zhou and Shiu-Kai Chin