The 14th International Conference on Theorem Proving in Higher Order Logics
3-6 September 2001, Edinburgh, Scotland

[Home Page][Conference History][Call for Papers][Guide for Authors][Programme] 
[Related Events][How to Get There][Weather and Tourism][Registration][Accommodation] 
[Sponsors][Student Bursaries][Proceedings][Photos][Business Meeting][TPHOLs 2002]

TPHOLs 2001 Programme

List of Presentations

Sunday, 2 September 2001

18:00-19:30 Registration and Reception

Registration and Reception, Castle Suite, Jury's Inn Hotel
Jury's Inn, 43 Jeffrey Street, Edinburgh, EH1 1DG

Monday, 3 September 2001

08:15-09:00 Registration

Registration at the University Conference and Training Centre
15 South College Street, Edinburgh

09:00-09:15 Conference Opening

Welcome and Opening Remarks
Richard Boulton, Conference Chair
Paul Jackson, Programme Chair

09:15-10:15 Invited Talk

Bart Jacobs, University of Nijmegen
JavaCard Program Verification

10:15-10:45 Coffee and Tea

10:45-12:00 Session A1

10:45-11:10
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, and Irene Schena
HELM and the Semantic Math-Web
11:10-11:35
Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, and Sam Owre
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS
11:35-12:00
Pavel Naumov, Mark-Oliver Stehr, and José Meseguer
The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability)

12:00-14:00 Lunch

Lunch today is not provided by the conference. Participants are free to arrange their own food from one of the many restaurants and sandwich bars in the vicinity of the conference venue.

14:00-16:00 Session B1: Work in Progress

14:00-15:15 Short Talks (5 minutes each)
15:15-16:00 Poster Session
Amr T. Abdel-Hamid, Sofiène Tahar, and John Harrison
Hierarchical Verification of the Implementation of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL
Hasan Amjad
BDD Representation Judgements in HOL: A Performance Evaluation
Pieter Audenaert
Toward a Verified Generic Prooftool
Stefan Berghofer and Tobias Nipkow
Executing Higher Order Logic
Pierre Castéran and Davy Rouillard
Towards a Generic Tool for Reasoning about Labeled Transition Systems
O. Celiku and J. von Wright
Transformational Reasoning with Incomplete Information
Sidi O. Ehmety and Lawrence C. Paulson
Representing Component States in Higher-Order Logic
Peter V. Homeier
Quotient Types
Christian Jacobi
Formal Verification of a Theory of IEEE Rounding
Savi Maharaj
A PVS Theory of Symbolic Transition Systems
Francisco Palomo-Lozano, Inmaculada Medina-Bulo, and José A. Alonso-Jiménez
Certification of Matrix Multiplication Algorithms
Claire L. Quigley
Proof for Optimization: Programming Logic Support for Java JIT Compilers
Elena Teica and Ranga Vemuri
Mechanizing in Higher-Order Logic Proofs of Correctness and Completeness for a Set of RTL Transformations
Haiyan Xiong, Paul Curzon, Sofiène Tahar, and Ann Blandford
Proving Existential Theorems when Importing Results from MDG to HOL
Dan Zhou and Paul E. Black
Translating HOL to Specifications for the Model Checker SMV

16:00-16:30 Coffee and Tea

16:30-17:45 Session A2

16:30-16:55
Pertti Kellomäki
A Structural Embedding of Ocsid in PVS
16:55-17:20
Giampaolo Bella and Lawrence C. Paulson
Mechanical Proofs about a Non-repudiation Protocol
17:20-17:45
Mark Bickford, Christoph Kreitz, Robbert van Renesse, and Xiaoming Liu
Proving Hybrid Protocols Correct

17:45 Close

Tuesday, 4 September 2001

08:30-09:00 Registration

Registration at the University Conference and Training Centre
15 South College Street, Edinburgh

09:00-10:15 Session A3

09:00-09:25
Xavier Rival and Jean Goubault-Larrecq
Experiments with Finite Tree Automata in Coq
09:25-09:50
Steffen Helke and Florian Kammüller
Representing Hierarchical Automata in Interactive Theorem Provers
09:50-10:15
Simon J. Gay
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL

10:15-10:45 Coffee and Tea

10:45-12:00 Session A4

10:45-11:10
J Strother Moore
Finite Set Theory in ACL2
11:10-11:35
David Hemer, Ian Hayes, and Paul Strooper
Refinement Calculus for Logic Programming in Isabelle/HOL
11:35-12:00
Matt Fairtlough, Michael Mendler, and Xiaochun Cheng
Abstraction and Refinement in Higher Order Logic

12:00-14:00 Lunch

Lunch today is not provided by the conference. Participants are free to arrange their own food from one of the many restaurants and sandwich bars in the vicinity of the conference venue.

14:00-16:00 Session B2: Work in Progress

14:00-15:15 Short Talks (5 minutes each)
15:15-16:00 Poster Session
Marcin Benke
Some Tools for Computer-Assisted Theorem Proving in Martin-Löf Type Theory
Christoph Benzmüller and Manfred Kerber
A Lost Proof
Olivier Boite and Catherine Dubois
Proving Type Soundness of a Simply Typed ML-Like Language with References
Paul Curzon and Ann Blandford
A User Model for Avoiding Design Induced Errors in Soft-Key Interactive Systems
Christophe Depasse
Constructing Isabelle Proofs in a Proof Refinement Calculus
John Harrison
Complex Quantifier Elimination in HOL
M. Randall Holmes
The Implementation of an Unusual Higher-Order Logic
Peter V. Homeier
A Proof of the Church-Rosser Theorem for the Lambda Calculus in Higher Order Logic
Joe Hurd
Verification of the Miller-Rabin Probabilistic Primality Test
A. Momigliano, S. J. Ambler, and R. L. Crole
A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle
Loïc Pottier
Quotients in the CIC
Thomas Marthedal Rasmussen
An Inductive Approach to Formalizing Notions of Number Theory Proofs
Vlad Rusu
Verifying that Invariants are Context-Inductive
Claudio Sacerdoti Coen
Tactics in Modern Proof-Assistants: The Bad Habit of Overkilling

16:00-16:30 Coffee and Tea

16:30-17:45 Session A5

16:30-16:55
Mario Cáccamo and Glynn Winskel
A Higher-Order Calculus for Categories
16:55-17:20
Ana Bove and Venanzio Capretta
Nested General Recursion and Partiality in Type Theory
17:20-17:45
Rob D. Arthan
An Irrational Construction of R from Z

17:45 Close

Wednesday, 5 September 2001

08:45-09:00 Joint Session Opening, Royal Museum of Scotland

[Conditions of Entry into the Museum]

Welcome and Opening Remarks
Tiziana Margaria, CHARME Programme Chair
Paul Jackson, TPHOLs Programme Chair

09:00-10:30 Joint Session Papers

09:00-09:30 (CHARME)
K. L. McMillan
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking
09:30-10:00 (TPHOLs)
Marc Daumas, Laurence Rideau, and Laurent Théry
A Generic Library for Floating-Point Numbers and its Application to Exact Computing
10:00-10:30 (CHARME)
Roope Kaivola and Katherine Kohatsu
Proof Engineering in the Large: Formal Verification of Pentium 4 Floating-Point Divider

10:30-11:00 Coffee and Tea

11:00-12:00 Invited Talk

Steven D. Johnson, Indiana University
View from the Fringe of the Fringe

A packed lunch will be provided today.

12:45 Coaches to Excursion at Traquair House leave from Royal Museum of Scotland

12:45-17:00
Excursion at Traquair House

17:00 Coaches to Edinburgh leave from Traquair House

19:30-23:00 Conference Banquet, Old College, University of Edinburgh

19:30-20:00
Reception
Raeburn Room, Old College, University of Edinburgh
South Bridge, Edinburgh, EH8 9YL
20:00-23:00
Dinner
Playfair Library Hall, Old College, University of Edinburgh
South Bridge, Edinburgh, EH8 9YL

Thursday, 6 September 2001

09:00-10:00 Invited Talk

Natarajan Shankar, SRI International
Using Decision Procedures with a Higher-Order Logic

10:00-10:30 Coffee and Tea

10:30-12:10 Session A6

10:30-10:55
Louise A. Dennis and Alan Smaill
Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
10:55-11:20
Inmaculada Medina-Bulo, Francisco Palomo-Lozano, and José A. Alonso-Jiménez
A Certified Polynomial-Based Decision Procedure for Propositional Logic
11:20-11:45
David Pichardie and Yves Bertot
Formalizing Convex Hull Algorithms
11:45-12:10
Venanzio Capretta
Certifying the Fast Fourier Transform with Coq

12:10-14:00 Lunch

Lunch today is not provided by the conference. Participants are free to arrange their own food from one of the many restaurants and sandwich bars in the vicinity of the conference venue.

14:00-15:15 Session A7

14:00-14:25
Joe Hurd
Predicate Subtyping with Predicate Sets
14:25-14:50
Gertrud Bauer and Markus Wenzel
Calculational Reasoning Revisited (An Isabelle/Isar Experience)
14:50-15:15
Freek Wiedijk
Mizar Light for HOL Light

15:15-15:45 Coffee and Tea

15:45-16:45 Business Meeting

16:45-17:00 Closing Remarks

17:00 Close