Skip to main content
SpringerLink
Log in

Interactive Theorem Proving

9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings

  • Conference proceedings
  • © 2018

Overview

Editors:
  1. Jeremy Avigad

    1. Carnegie Mellon University, Pittsburgh, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Assia Mahboubi

    1. Inria, Nantes, France

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

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

Included in the following conference series:

Conference proceedings info: ITP 2018.

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 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 99.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 (38 papers)

  1. Front Matter

    Pages I-XVII
    Download chapter PDF

  2. Physical Addressing on Real Hardware in Isabelle/HOL

    • Reto Achermann, Lukas Humbel, David Cock, Timothy Roscoe
    Pages 1-19

  3. Towards Certified Meta-Programming with Typed Template-Coq

    • Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
    Pages 20-39Open Access

  4. Formalizing Ring Theory in PVS

    • Andréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino
    Pages 40-47

  5. Software Tool Support for Modular Reasoning in Modal Logics of Actions

    • Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
    Pages 48-67

  6. Backwards and Forwards with Separation Logic

    • Callum Bannister, Peter Höfner, Gerwin Klein
    Pages 68-87

  7. A Coq Formalisation of SQL’s Execution Engines

    • V. Benzaken, É. Contejean, Ch. Keller, E. Martins
    Pages 88-107

  8. A Coq Tactic for Equality Learning in Linear Arithmetic

    • Sylvain Boulmé, Alexandre Maréchal
    Pages 108-125

  9. The Coinductive Formulation of Common Knowledge

    • Colm Baston, Venanzio Capretta
    Pages 126-141

  10. Tactics and Certificates in Meta Dedukti

    • Raphaël Cauderlier
    Pages 142-159

  11. A Formalization of the LLL Basis Reduction Algorithm

    • Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
    Pages 160-177Open Access

  12. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs

    • Christian Doczkal, Guillaume Combette, Damien Pous
    Pages 178-195

  13. Verified Analysis of Random Binary Tree Structures

    • Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
    Pages 196-214

  14. HOL Light QE

    • Jacques Carette, William M. Farmer, Patrick Laskowski
    Pages 215-234

  15. Efficient Mendler-Style Lambda-Encodings in Cedille

    • Denis Firsov, Richard Blair, Aaron Stump
    Pages 235-252

  16. Verification of PCP-Related Computational Reductions in Coq

    • Yannick Forster, Edith Heiter, Gert Smolka
    Pages 253-269

  17. ProofWatch: Watchlist Guidance for Large Theories in E

    • Zarathustra Goertzel, Jan Jakubův, Stephan Schulz, Josef Urban
    Pages 270-288

  18. Reification by Parametricity

    • Jason Gross, Andres Erbsen, Adam Chlipala
    Pages 289-305

  19. Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata

    • Simon Jantsch, Michael Norrish
    Pages 306-323

  20. CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math”

    • Wolfram Kahl
    Pages 324-341
Back to top

Other volumes

  1. Interactive Theorem Proving

Keywords

About this book

This book constitutes the refereed proceedings of the 9th International Conference on Interactive Theorem Proving, ITP 2018, held in Oxford, UK, in July 2018.

The 32 full papers and 5 short papers presented were carefully reviewed and selected from 65 submissions.  The papers feature research in the area of logical frameworks and interactive proof assistants. The topics include theoretical foundations and implementation aspects of the technology, as well as applications to verifying hardware and software systems to ensure their safety and security, and applications to the formal verication of mathematical results.

Chapters 2, 10, 26, 29, 30 and 37 are available open access under a Creative Commons Attribution 4.0 International License via link.springer.com.


Editors and Affiliations

  • Carnegie Mellon University, Pittsburgh, USA

    Jeremy Avigad

  • Inria, Nantes, France

    Assia Mahboubi

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation