TPHOLs'99: Accepted Papers

A HOL Conversion for Translating Linear Time Temporal Logic to Omega-automata,

Klaus Schneider and Dirk W. Hoffmann

 

A machine-checked theory of floating point arithmetic,

John R. Harrison

 

Disjoint Sums over Type Classes in HOL,

Norbert Völker

 

From I/O Automata to timed I/O automata,

Bernd Grobauer and Olaf Müller

 

Hardware Verification using Co-induction in Coq,

Solange Coupet-Grimal and Line Jakubiec

 

Importing MDG Results into HOL,

Haiyan Xiong, Paul Curzon, Sofiène Tahar

 

Inductive datatypes in HOL - lessons learned in Formal-Logic Engineering,

Stefan Berghofer and Markus Wenzel

 

Integrating Gandalf and HOL,

Joe Hurd

 

Isar - a generic interpretative approach to readable formal proof documents,

Markus Wenzel

 

Isomorphisms - A Link Between the Shallow and the Deep,

Thomas Santen

 

Lifted-FL: A pragmatic Implementation of Combined Model Checking and Theorem Proving,

Mark D. Aagaard, Robert B. Jones and Carl-Johan H. Seger

 

Locales - A sectioning concept for Isabelle,

Florian Kammüller, Markus Wenzel and Lawrence C. Paulson

 

Mechanized Operational Semantics via (Co)Induction,

Simon J. Ambler and Roy L. Crole

 

On the Implementation of an Extensible Declarative Proof Language,

Vincent Zammit

 

Polytypic Proof Construction,

Holger Pfeifer and Harald Ruess

 

Recursive Function Definition over Coinductive Types,

John Matthews

 

Representing WP Semantics in Isabelle/ZF,

Mark Staples

 

Symbolic Functional Evaluation,

Nancy A. Day and Jeffrey J. Joyce

 

Three Tactic Theorem Proving,

Don Syme

 

Universal Algebra in Type Theory,

Venanzio Capretta

TPHOLs'99: Work-in-Progress Papers

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