Skip to main content
SpringerLink
Log in
Book cover

Interactive Theorem Proving

8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings

  • Conference proceedings
  • © 2017

Overview

Editors:
  1. Mauricio Ayala-Rincón

    1. University of Brasília, Brasília D.F., Brazil

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. César A. Muñoz

    1. NASA, Hampton, USA

    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 10499)

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

Included in the following conference series:

Conference proceedings info: ITP 2017.

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

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and 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

Table of contents (32 papers)

  1. Front Matter

    Pages i-xix
    Download chapter PDF

  2. Automated Theory Exploration for Interactive Theorem Proving:

    • Moa Johansson
    Pages 1-11

  3. Automating Formalization by Statistical and Semantic Parsing of Mathematics

    • Cezary Kaliszyk, Josef Urban, Jiří Vyskočil
    Pages 12-27

  4. A Formalization of Convex Polyhedra Based on the Simplex Method

    • Xavier Allamigeon, Ricardo D. Katz
    Pages 28-45

  5. A Formal Proof of the Expressiveness of Deep Learning

    • Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
    Pages 46-64

  6. Formalization of the Lindemann-Weierstrass Theorem

    • Sophie Bernard
    Pages 65-80

  7. CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics

    • Frédéric Besson, Sandrine Blazy, Pierre Wilke
    Pages 81-97

  8. Formal Verification of a Floating-Point Expansion Renormalization Algorithm

    • Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu
    Pages 98-113

  9. How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation

    • David Butler, David Aspinall, Adrià Gascón
    Pages 114-130

  10. FoCaLiZe and Dedukti to the Rescue for Proof Interoperability

    • Raphaël Cauderlier, Catherine Dubois
    Pages 131-147

  11. A Formal Proof in Coq of LaSalle’s Invariance Principle

    • Cyril Cohen, Damien Rouhling
    Pages 148-163

  12. How to Get More Out of Your Oracles

    • Luís Cruz-Filipe, Kim S. Larsen, Peter Schneider-Kamp
    Pages 164-170

  13. Certifying Standard and Stratified Datalog Inference Engines in SSReflect

    • Véronique Benzaken, Évelyne Contejean, Stefania Dumbrava
    Pages 171-188

  14. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq

    • Yannick Forster, Gert Smolka
    Pages 189-206

  15. Bellerophon: Tactical Theorem Proving for Hybrid Systems

    • Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer
    Pages 207-224

  16. Formalizing Basic Quaternionic Analysis

    • Andrea Gabrielli, Marco Maggesi
    Pages 225-240

  17. A Formalized General Theory of Syntax with Bindings

    • Lorenzo Gheri, Andrei Popescu
    Pages 241-261

  18. Proof Certificates in PVS

    • Frédéric Gilbert
    Pages 262-268

  19. Efficient, Verified Checking of Propositional Proofs

    • Marijn Heule, Warren Hunt Jr., Matt Kaufmann, Nathan Wetzler
    Pages 269-284

  20. Proof Tactics for Assertions in Separation Logic

    • Zhé Hóu, David Sanán, Alwen Tiu, Yang Liu
    Pages 285-303
Back to top

Other volumes

  1. Interactive Theorem Proving

Keywords

About this book

This book constitutes the refereed proceedings of the 8th International Conference on Interactive Theorem Proving, ITP 2017, held in Brasilia, Brazil, in September 2017.

The 28 full papers, 2 rough diamond papers, and 3 invited talk papers presented were carefully reviewed and selected from 65 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematical theories.

Editors and Affiliations

  • University of Brasília, Brasília D.F., Brazil

    Mauricio Ayala-Rincón

  • NASA, Hampton, USA

    César A. Muñoz

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation