Skip to main content
  • Conference proceedings
  • © 2007

Theorem Proving in Higher Order Logics

20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings

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

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Conference series link(s): TPHOLs: International Conference on Theorem Proving in Higher Order Logics

Conference proceedings info: TPHOLs 2007.

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 (28 papers)

  1. Front Matter

  2. Separation Logic for Small-Step cminor

    • Andrew W. Appel, Sandrine Blazy
    Pages 5-21
  3. Formalising Java’s Data Race Free Guarantee

    • David Aspinall, Jaroslav Ševčík
    Pages 22-37
  4. Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL

    • Lukas Bulwahn, Alexander Krauss, Tobias Nipkow
    Pages 38-53
  5. Formalising Generalised Substitutions

    • Jeremy E. Dawson
    Pages 54-69
  6. Extracting Purely Functional Contents from Logical Inductive Types

    • David Delahaye, Catherine Dubois, Jean-Frédéric Étienne
    Pages 70-85
  7. A Modular Formalisation of Finite Group Theory

    • Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
    Pages 86-101
  8. A Formally Verified Prover for the \(\mathcal{ALC\,}\) Description Logic

    • José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesus Martín-Mateos, José-Luis Ruiz-Reina
    Pages 135-150
  9. Using XCAP to Certify Realistic Systems Code: Machine Context Management

    • Zhaozhong Ni, Dachuan Yu, Zhong Shao
    Pages 189-206
  10. Proof Pearl: De Bruijn Terms Really Do Work

    • Michael Norrish, René Vestergaard
    Pages 207-222
  11. Proof Pearl: Looping Around the Orbit

    • Steven Obua
    Pages 223-231
  12. Source-Level Proof Reconstruction for Interactive Theorem Proving

    • Lawrence C. Paulson, Kong Woei Susanto
    Pages 232-245

Other Volumes

  1. Theorem Proving in Higher Order Logics

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