Skip to main content
  • Conference proceedings
  • © 1999

Theorem Proving in Higher Order Logics

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

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 1690)

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (23 papers)

  1. Front Matter

    Pages I-VIII
  2. Disjoint Sums over Type Classes in HOL

    • Norbert Völker
    Pages 5-18
  3. Polytypic Proof Construction

    • Holger Pfeifer, Harald Rueβ
    Pages 55-72
  4. Hardware Verification Using Co-induction in COQ

    • Solange Coupet-Grimal, Line Jakubiec
    Pages 91-108
  5. Connecting Proof Checkers and Computer Algebra Using OpenMath

    • Olga Caprotti, Arjeh M. Cohen
    Pages 109-112
  6. Universal Algebra in Type Theory

    • Venanzio Capretta
    Pages 131-148
  7. Locales A Sectioning Concept for Isabelle

    • Florian Kammüller, Markus Wenzel, Lawrence C. Paulson
    Pages 149-165
  8. Three Tactic Theorem Proving

    • Don Syme
    Pages 203-220
  9. Mechanized Operational Semantics via (Co)Induction

    • Simon J. Ambler, Roy L. Crole
    Pages 221-238
  10. Representing WP Semantics in Isabelle/ZF

    • Mark Staples
    Pages 239-254
  11. A HOL Conversion for Translating Linear Time Temporal Logic to ω-Automata

    • Klaus Schneider, Dirk W. Hoffmann
    Pages 255-272
  12. From I/O Automata to Timed I/O Automata

    • Bernd Grobauer, Olaf Müller
    Pages 273-289
  13. Formal Methods and Security Evaluation

    • Dominique Bolignano
    Pages 291-291

Editors and Affiliations

  • INRIA Sophia Antipolis, Sophia Antipolis Cedex, France

    Yves Bertot, Gilles Dowek, Laurent Théry

  • University of Nice - Sophia Antipolis, Nice Cedex 2, France

    André Hirschowitz

  • University of Paris XI, Orsay Cedex, France

    Christine Paulin

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access