Theorem Proving in Higher Order Logics: 16th International Conference, Tphols 2003, Rome, Italy, September 8-12, 2003 : Proceedings

by Tphols 200 (2003 Rome, Italy); Wolff, Burkhart

• ISBN13: 9783540406648
• ISBN10: 3540406646
• Format: Paperback
• Copyright: 2003-09-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2003, held in Rome, Italy in September 2003. The 24 revised full papers presented together with an invited paper were carefully reviewed and selected from 50 submissions. The papers are organized in topical sections on hardware and Assembler languages, proof automation, fool combination, logic extensions, theorem prover technology, mathematical theories, and security. Among the theorem proving systems discussed are HOL, Coq, MetaPRL, and Isabelle/Isar.

Table of Contents

Invited Talk I
Click'n Prove: Interactive Proofs within Set Theory	1	(24)
Jean-Raymond Abrial
Dominique Cansell
Hardware and Assembler Languages
Formal Specification and Verification of ARM6	25	(16)
Anthony Fox
A Programming Logic for Java Bytecode Programs	41	(14)
Claire L. Quigley
Verified Bytecode Subroutines	55	(16)
Gerwin Klein
Martin Wildmoser
Proof Automation I
Complete Integer Decision Procedures as Derived Rules in HOL	71	(16)
Michael Norrish
Changing Data Representation within the Coq System	87	(16)
Nicolas Magaud
Applications of Polytypism in Theorem Proving	103	(17)
Konrad Slind
Joe Hurd
Proof Automation II
A Coverage Checking Algorithm for LF	120	(16)
Carsten Schurmann
Frank Pfenning
Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions	136	(19)
Deepak Kapur
Nikita A. Sakhanenko
Tool Combination
Embedding of Systems of Affine Recurrence Equations in Coq	155	(16)
David Cachera
David Pichardie
Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover	171	(17)
Hasan Amjad
Combining Testing and Proving in Dependent Type Theory	188	(16)
Peter Dybjer
Qiao Haiyan
Makoto Takeyama
Invited Talk II
Reasoning about Proof Search Specifications: An Abstract	204	(1)
Dale Miller
Logic Extensions
Program Extraction from Large Proof Developments	205	(16)
Luis Cruz-Filipe
Bas Spitters
First Order Logic with Domain Conditions	221	(17)
Freek Wiedijk
Jan Zwanenburg
Extending Higher-Order Unification to Support Proof Irrelevance	238	(15)
Jason Reed
Advances in Theorem Prover Technology
Inductive Invariants for Nested Recurision	253	(17)
Sava Krstic
John Matthews
Implementing Modules in the Coq System	270	(17)
Jacek Chrzaszcz
MetaPRL - A Modular Logical Environment	287	(17)
Jason Hickey
Aleksey Nogin
Robert L. Constable
Brian E. Aydemir
Eli Barzilay
Yegor Bryukhov
Richard Eaton
Adam Granicz
Alexei Kopylov
Christoph Kreitz
Vladimir N. Krupski
Lori Lorigo
Stephan Schmitt
Carl Witty
Xin Yu
Mathematical Theories
Proving Pearl: Knuth's Algorithm for Prime Numbers	304	(15)
Laurent Thery
Formalizing Hilbert's Grundlagen in Isabelle/Isar	319	(16)
Laura I. Meikle
Jacques D. Fleuriot
Security
Using Coq to Verify Java Card™ Applet Isolation Properties	335	(17)
June Andronick
Boutheina Chetali
Olivier Ly
Verifying Second-Level Security Protocols	352	(15)
Giampaolo Bella
Cristiano Longo
Lawrence C Paulson
Author Index	367