iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/3-540-45685-6
Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings | SpringerLink
Skip to main content
Springer Nature Link
Log in

Theorem Proving in Higher Order Logics

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

  • Conference proceedings
  • © 2002

Overview

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)

Included in the following conference series:

Conference proceedings info: TPHOLs 2002.

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

Access this book

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy 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

Licence this eBook for your library

Institutional subscriptions

Keywords

Table of contents (22 papers)

  1. Front Matter

    Pages I-X
    Download chapter 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

    7. Explicit Universes for the Calculus of Constructions

      • Judicaël Courant
      Pages 115-130

    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

    13. PuzzleTool: An Example of Programming Computation and Deduction

      • Michael J. C. Gordon
      Pages 214-229

    14. A Formal Approach to Probabilistic Termination

      • Joe Hurd
      Pages 230-245

    15. Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm

      • Micaela Mayero
      Pages 246-262

    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

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

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

Publish with us

Policies and ethics

Back to top

Search

Navigation