Yves Bertot

G. Kahn

Laurent Théry

Abstract: "This paper presents a principle for a natural and effective use of the mouse in the user-interface of computer proof assistants."

Proof by Pointing

Examines the significance of Gilles Kahn's contribution to computer science and reflects upon the future development of information technology.

Essays in Honour of Gilles Kahn

From Semantics to Computer Science

Gilles Dowek

Andre Hirschowitz

Christine Paulin

Laurent Thery

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.

12th International Conference, TPHOLs'99, Nice, France, September 14-17, 1999, Proceedings

Theorem Proving in Higher Order Logics

Pierre Castéran

A practical introduction to the development of proofs and certified programs using Coq. An invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.

Yves Bertot

Books

Your next favorite book is out there