This book constitutes the refereed proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '99, held in Nice, France, in September 1999. The 20 revised full papers presented together with three invited contributions were carefully reviewed and selected from 35 papers submitted. All current aspects of higher order theorem proving, formal verification, and specification are discussed. Among the theorem provers evaluated are COQ, HOL, Isabelle, Isabelle/ZF, and OpenMath.
Author(s): Thomas Kropf (auth.), Yves Bertot, Gilles Dowek, Laurent Théry, André Hirschowitz, Christine Paulin (eds.)
Series: Lecture Notes in Computer Science 1690
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1999
Language: English
Pages: 364
Tags: Applications of Mathematics; Mathematical Software; Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Artificial Intelligence (incl. Robotics); Software Engineering
Front Matter....Pages I-VIII
Recent Advancements in Hardware Verification — How to Make Theorem Proving Fit for an Industrial Usage....Pages 1-4
Disjoint Sums over Type Classes in HOL....Pages 5-18
Inductive Datatypes in HOL — Lessons Learned in Formal-Logic Engineering....Pages 19-36
Isomorphisms — A Link Between the Shallow and the Deep....Pages 37-54
Polytypic Proof Construction....Pages 55-72
Recursive Function Definition over Coinductive Types....Pages 73-90
Hardware Verification Using Co-induction in COQ....Pages 91-108
Connecting Proof Checkers and Computer Algebra Using OpenMath ....Pages 109-112
A Machine-Checked Theory of Floating Point Arithmetic....Pages 113-130
Universal Algebra in Type Theory....Pages 131-148
Locales A Sectioning Concept for Isabelle....Pages 149-165
Isar — A Generic Interpretative Approach to Readable Formal Proof Documents....Pages 167-183
On the Implementation of an Extensible Declarative Proof Language....Pages 185-202
Three Tactic Theorem Proving....Pages 203-220
Mechanized Operational Semantics via (Co)Induction....Pages 221-238
Representing WP Semantics in Isabelle/ZF....Pages 239-254
A HOL Conversion for Translating Linear Time Temporal Logic to ω-Automata....Pages 255-272
From I/O Automata to Timed I/O Automata....Pages 273-289
Formal Methods and Security Evaluation....Pages 291-291
Importing MDG Verification Results into HOL....Pages 293-310
Integrating Gandalf and HOL....Pages 311-321
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving....Pages 323-340
Symbolic Functional Evaluation....Pages 341-358
Back Matter....Pages 359-359
