Accepted Papers

Regular Papers

  1. Jean-François Dufourd. Hypermap Specification and Certified Linked Implementation using Orbits.
  2. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu and Dmitriy Traytel. Truly Modular (Co)datatypes for Isabelle/HOL.
  3. Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel. Cardinals in Isabelle/HOL. (Slides)
  4. Jason Gross, Adam Chlipala and David Spivak. Experience Implementing a Performant Category-Theory Library in Coq.
  5. J Strother Moore. Proof Pearl: Proving a Simple von Neumann Machine Turing Complete.
  6. Makarius Wenzel. Asynchronous User Interaction and Tool Integration in Isabelle/PIDE.
  7. Kento Emoto, Frédéric Loulergue and Julien Tesson. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction.
  8. Guyslain Naves and Arnaud Spiwack. Balancing lists: a proof pearl.
  9. Sandrine Blazy, Vincent Laporte and David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. (Slides)
  10. Tobias Nipkow and Dmitriy Traytel. Unified Decision Procedures for Regular Expression Equivalence.
  11. Peter Lammich. Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm.
  12. Ramana Kumar, Rob Arthan, Magnus O. Myreen and Scott Owens. HOL with Definitions: Semantics, Soundness, and a Verified Implementation.
  13. Gregory Malecha, Adam Chlipala and Thomas Braibant. Compositional Computational Reflection.
  14. Matthieu Sozeau and Nicolas Tabareau. Universe Polymorphism in Coq.
  15. Daniel Matichuk, Toby Murray and Makarius Wenzel. An Isabelle Proof Method Language.
  16. Magnus O. Myreen and Jared Davis. The reflective Milawa theorem prover is sound (down to the machine code that runs it).
  17. David Cock. Proof Pearl: From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle.
  18. Vincent Aravantinos and Sofiene Tahar. Implicational Rewriting Tactics in HOL. (Slides)
  19. Timothy Bourke, Rob Van Glabbeek and Peter Höfner. Showing invariance compositionally for a process algebra of network protocols.
  20. Andreas Lochbihler and Johannes Hölzl. Recursive Functions on Codatatypes via Domains and Topologies.
  21. Christian Doczkal and Gert Smolka. Completeness and Decidability Results for CTL in Coq. (Slides)
  22. Evmorfia-Iro Bartzia and Pierre-Yves Strub. A Formal Library for Elliptic Curves in the Coq Proof Assistant.
  23. Nao Hirokawa, Aart Middeldorp and Christian Sternagel. A New and Formalized Proof of Abstract Completion.
  24. Cyril Cohen and Anders Mörtberg. A Coq Formalization of Finitely Presented Modules.
  25. Martin Ring and Christoph Lüth. Collaborative Interactive Theorem Proving with Clide. (Slides)
  26. Umair Siddique, Mohamed Yousri Mahmoud and Sofiene Tahar. On the Formalization of Z-Transform in HOL.
  27. Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote and Enrico Tassi. A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3).
  28. Mohamed Yousri Mahmoud, Vincent Aravantinos and Sofiene Tahar. Formal Verification of Optical Quantum Flip Gate.
  29. Jeremy Avigad, Robert Y. Lewis and Cody Roux. A heuristic prover for real inequalities.
  30. Abhishek Anand and Vincent Rahli. Towards a Formally Verified Proof Assistant.
  31. Robert Dockins. Formalized, effective domain theory in Coq.

Rough Diamonds

  1. Matt Kaufmann and J Moore. Rough Diamond: An Extension of Equivalence-based Rewriting.
  2. Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C semantics: CompCert and the C standard.
  3. Disha Puri, Sandip Ray, Kecheng Hao and Fei Xie. Mechanical Certification of Loop Pipelining Transformations: A Preview.
  4. Rob Arthan. HOL Constant Definitions Done Right.