[TPHOLs'99 Home Page] [Call for Papers] [Guide for Authors] [Accepted Papers] [Supplementary Proceedings] [Conference History] [Conference Schedule] [How to Get There] [Weather and Tourism]

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

[TPHOLs'99 Home Page] [Call for Papers] [Guide for Authors] [Accepted Papers] [Supplementary Proceedings] [Conference History] [Conference Schedule] [How to Get There] [Weather and Tourism]

Comments and Feedback: TPHOLs99@sophia.inria.fr
Author: The TPHOLs'99 Organising Committee
Date Last Modified: Wed 31 May 2000
URL: accepted.html