• John Harrison
Part of the Distinguished Dissertations book series (DISTDISS)


We briefly survey the field of computer theorem proving and emphasize the recent interest in using theorem provers for the verification of computer systems. We point out a significant hole in existing practice, where verification of many interesting systems cannot be performed for lack of mathematical infrastructure concerning the real numbers and classical ‘continuous’ mathematics. This motivates the remainder of the book where we show how to plug this gap, and illustrate the possibilities with some applications.


Model Check Theorem Prove Computer Algebra System High Order Logic Denotational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London Limited 1998

Authors and Affiliations

  • John Harrison
    • 1
  1. 1.New Museums SiteUniversity of Cambridge Computer LaboratoryCambridgeUK

Personalised recommendations