Skip to main content
SpringerLink
Log in
Book cover
  • Conference proceedings
  • © 2002

Theorem Proving in Higher Order Logics

15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings

Editors:

  1. Victor A. Carreño

    1. NASA Langley Research Center, Hampton, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. César A. Muñoz

    1. ICASE-Langley Research Center, Hampton, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Sofiène Tahar

    1. Electrical and Computer Engineering, Concordia University, Montréal, Canada

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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

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

Conference proceedings info: TPHOLs 2002.

Sections

Buy it now

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

  1. Front Matter

    Pages I-X
    PDF

  2. Invited Talks

    1. Formal Methods at NASA Langley

      • Ricky Butler
      Pages 1-2

    2. Higher Order Unification 30 Years Later

      • Gérard Huet
      Pages 3-12

  3. Regular Papers

    1. Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction

      • Simon J. Ambler, Roy L. Crole, Alberto Momigliano
      Pages 13-30

    2. Efficient Reasoning about Executable Specifications in Coq

      • Gilles Barthe, Pierre Courtieu
      Pages 31-46

    3. Verified Bytecode Model Checkers

      • David Basin, Stefan Friedrich, Marek Gawkowski
      Pages 47-66

    4. The 5 Colour Theorem in Isabelle/Isar

      • Gertrud Bauer, Tobias Nipkow
      Pages 67-82

    5. Type-Theoretic Functional Semantics

      • Yves Bertot, Venanzio Capretta, Kuntal Das Barman
      Pages 83-97

    6. A Proposal for a Formal OCL Semantics in Isabelle/HOL

      • Achim D. Brucker, Burkhart Wolff
      Pages 99-114

    8. Formalised Cut Admissibility for Display Logic

      • Jeremy E. Dawson, Rajeev Goré
      Pages 131-147

    9. Formalizing the Trading Theorem for the Classification of Surfaces

      • Christophe Dehlinger, Jean-François Dufourd
      Pages 148-163

    10. Free-Style Theorem Proving

      • David Delahaye
      Pages 164-181

    11. A Comparison of Two Proof Critics: Power vs. Robustness

      • Louise A. Dennis, Alan Bundy
      Pages 182-197

    12. Two-Level Meta-reasoning in Coq

      • Amy P. Felty
      Pages 198-213

    16. Quotient Types: A Modular Approach

      • Aleksey Nogin
      Pages 263-280

    17. Sequent Schema for Derived Rules

      • Aleksey Nogin, Jason Hickey
      Pages 281-297
Back to top

Other Volumes

  1. Theorem Proving in Higher Order Logics

Back to top

Keywords

Back to top

Editors and Affiliations

  • NASA Langley Research Center, Hampton, USA

    Victor A. Carreño

  • ICASE-Langley Research Center, Hampton, USA

    César A. Muñoz

  • Electrical and Computer Engineering, Concordia University, Montréal, Canada

    Sofiène Tahar

Back to top

Bibliographic Information

  • Book Title: Theorem Proving in Higher Order Logics

  • Book Subtitle: 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings

  • Editors: Victor A. Carreño, César A. Muñoz, Sofiène Tahar

  • Series Title: Lecture Notes in Computer Science

  • DOI: https://doi.org/10.1007/3-540-45685-6

  • Publisher: Springer Berlin, Heidelberg

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer-Verlag Berlin Heidelberg 2002

  • Softcover ISBN: 978-3-540-44039-0Published: 07 August 2002

  • eBook ISBN: 978-3-540-45685-8Published: 02 August 2003

  • Series ISSN: 0302-9743

  • Series E-ISSN: 1611-3349

  • Edition Number: 1

  • Number of Pages: X, 347

  • Topics: Computer System Implementation, Theory of Computation, Software Engineering, Logic Design

Back to top

Publish with us

Policies and ethics

Back to top
Access via your institution

Buy it now

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

Search

Navigation