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

  • Jeremy Avigad
  • Assia Mahboubi
Conference proceedings ITP 2018

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

Also part of the Theoretical Computer Science and General Issues book sub series (LNTCS, volume 10895)

Table of contents

  1. Front Matter
    Pages I-XVII
  2. Reto Achermann, Lukas Humbel, David Cock, Timothy Roscoe
    Pages 1-19
  3. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
    Pages 20-39 Open Access
  4. Andréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino
    Pages 40-47
  5. Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
    Pages 48-67
  6. Callum Bannister, Peter Höfner, Gerwin Klein
    Pages 68-87
  7. V. Benzaken, É. Contejean, Ch. Keller, E. Martins
    Pages 88-107
  8. Sylvain Boulmé, Alexandre Maréchal
    Pages 108-125
  9. Colm Baston, Venanzio Capretta
    Pages 126-141
  10. Raphaël Cauderlier
    Pages 142-159
  11. Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
    Pages 160-177 Open Access
  12. Christian Doczkal, Guillaume Combette, Damien Pous
    Pages 178-195
  13. Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
    Pages 196-214
  14. Jacques Carette, William M. Farmer, Patrick Laskowski
    Pages 215-234
  15. Denis Firsov, Richard Blair, Aaron Stump
    Pages 235-252
  16. Yannick Forster, Edith Heiter, Gert Smolka
    Pages 253-269
  17. Zarathustra Goertzel, Jan Jakubův, Stephan Schulz, Josef Urban
    Pages 270-288
  18. Jason Gross, Andres Erbsen, Adam Chlipala
    Pages 289-305
  19. Alexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer
    Pages 342-361
  20. Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen
    Pages 362-369
  21. Andreas Lochbihler
    Pages 388-410
  22. Andreas Lochbihler, Joshua Schneider
    Pages 411-431
  23. Alexandra Mendes, João F. Ferreira
    Pages 432-440
  24. Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
    Pages 441-458 Open Access
  25. Étienne Miquey
    Pages 459-476
  26. Mariano M. Moscato, Carlos G. Lopez Pombo, César A. Muñoz, Marco A. Feliú
    Pages 477-494
  27. Julian Parsert, Cezary Kaliszyk
    Pages 495-503 Open Access
  28. João Paulo Pizani Flor, Wouter Swierstra
    Pages 504-522 Open Access
  29. Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic
    Pages 523-541
  30. Hira Taqdees Syeda, Gerwin Klein
    Pages 542-559
  31. Joseph Tassarotti, Robert Harper
    Pages 560-578
  32. Simon Wimmer, Shuwei Hu, Tobias Nipkow
    Pages 579-596
  33. Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers
    Pages 604-622
  34. Ran Zmigrod, Matthew L. Daggitt, Timothy G. Griffin
    Pages 623-639 Open Access
  35. Jeremy Avigad, Assia Mahboubi
    Pages E1-E1
  36. Back Matter
    Pages 641-642

About these proceedings


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


artificial intelligence automated reasoning code generation formal logic formal methods formal verifications graph theory Interactive proof systems isabelle/hol model checking problem solving program compilers programming languages semantics software engineering software evaluation specifications theorem provers theorem proving verification

Editors and affiliations

  • Jeremy Avigad
    • 1
  • Assia Mahboubi
    • 2
  1. 1.Carnegie Mellon UniversityPittsburghUSA
  2. 2.InriaNantesFrance

Bibliographic information

Industry Sectors
IT & Software