Theorem Proving in Higher Order Logics : 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings

by Boulton, Richard J.; Jackson, Paul B.

• ISBN13: 9783540425250
• ISBN10: 354042525X
• Format: Paperback
• Copyright: 2001-09-01
• Publisher: Springer Verlag

Summary

This book constitutes the thoroughly refereed proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001, held in Edinburgh, Scotlang, UK in September 2001. The 23 revised full papers presented together with one invited paper and two invited abstracts were carefully reviewed and selected from a total of 47 submissions. All current issues in HOL theorem proving and formal verification of hardware and software systems are addressed. Among the HOL theorem proving systems evaluated are Coq, HOL, Isabelle, and PVS.

Table of Contents

Invited Talks
JavaCard Program Verification	1	(3)
Bart Jacobs
View from the Fringe of the Fringe (Joint with CHARME 2001)	4	(1)
Steven D. Johnson
Using Decision Procedures with a Higher-Order Logic	5	(22)
Natarajan Shankar
Regular Contributions
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS	27	(16)
Andrew Adams
Martin Dunstan
Hanne Gottliebsen
Tom Kelsey
Ursula Martin
Sam Owre
An Irrational Construction of R from Z	43	(16)
Rob D. Arthan
HELM and the Semantic Math-Web	59	(16)
Andrea Asperti
Luca Padovani
Claudio Sacerdoti Coen
Irene Schena
Calculational Reasoning Revisited (An Isabelle/Isar Experience)	75	(16)
Gertrud Bauer
Markus Wenzel
Mechanical Proofs about a Non-repudiation Protocol	91	(14)
Giampaolo Bella
Lawrence C. Paulson
Proving Hybrid Protocols Correct	105	(16)
Mark Bickford
Christoph Kreitz
Robbert van Renesse
Xiaoming Liu
Nested General Recursion and Partiality in Type Theory	121	(15)
Ana Bove
Venanzio Capretta
A Higher-Order Calculus for Categories	136	(18)
Mario Caccamo
Glynn Winskel
Certifying the Fast Fourier Transform with Coq	154	(15)
Venanzio Capretta
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing	169	(16)
Marc Daumas
Laurence Rideau
Gaurent Thery
Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain	185	(16)
Louise A. Dennis
Alan Smaill
Abstraction and Refinement in Higher Order Logic	201	(16)
Matt Fairtlough
Michael Mendler
Xiaochun Cheng
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL	217	(16)
Simon J. Gay
Representing Hierarchical Automata in Interactive Theorem Provers	233	(16)
Steffen Helke
Florian Kammuller
Refinement Calculus for Logic Programming in Isabelle/HOL	249	(16)
David Hemer
Ian Hayes
Paul Strooper
Predicate Subtyping with Predicate Sets	265	(16)
Joe Hurd
A Structural Embedding of Ocsid in PVS	281	(16)
Pertti Kellomaki
A Certified Polynomial-Based Decision Procedure for Propositional Logic	297	(16)
Inmaculada Medina-Bulo
Francisco Palomo-Lozano
Jose A. Alonso-Jimenez
Finite Set Theory in ACL2	313	(16)
J Strother Moore
The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability)	329	(17)
Pavel Naumov
Mark-Oliver Stehr
Jose Meseguer
Formalizing Convex Hull Algorithms	346	(16)
David Pichardie
Yves Bertot
Experiments with Finite Tree Automata in Coq	362	(16)
Xavier Rival
Jean Goubault-Larrecq
Mizar Light for HOL Light	378	(17)
Freek Wiedijk
Author Index	395