| Monday, July 14th |
| Session 24C 10:45-13:00 |
| 10:45-11:15 | Abhishek Anand and Vincent Rahli. Towards a Formally Verified Proof Assistant (Slides) |
|---|
| 11:15-11:45 | Magnus O. Myreen and Jared Davis. The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Slides) |
|---|
| 11:45-12:15 | Ramana Kumar, Rob Arthan, Magnus O. Myreen and Scott Owens. HOL with Definitions: Semantics, Soundness, and a Verified Implementation (Slides) |
|---|
| 12:15-12:45 | J Strother Moore. Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (Slides) |
|---|
| 12:45-13:00 | Matt Kaufmann and J Moore. Rough Diamond: An Extension of Equivalence-based Rewriting (Slides) |
|---|
| Session 27B 14:30-16:00 |
| 14:30-15:00 | David Cock. From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle |
|---|
| 15:00-16:00 | Anna Slobodova, Jared Davis and Sol Swords. Microcode Verification - Another Piece of the Microprocessor Verification Puzzle |
|---|
| Session 28C 16:30-18:00 |
| 16:30-17:00 | Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu and Dmitriy Traytel. Truly Modular (Co)datatypes for Isabelle/HOL (Slides) |
|---|
| 17:00-17:30 | Andreas Lochbihler and Johannes Hölzl. Recursive Functions on Codatatypes via Domains and Topologies (Slides) |
|---|
| 17:30-18:00 | Jason Gross, Adam Chlipala and David Spivak. Experience Implementing a Performant Category-Theory Library in Coq (Slides) |
|---|
| Tuesday, July 15th |
| Session 33C 10:45-13:00 |
| 10:45-11:15 | Evmorfia-Iro Bartzia and Pierre-Yves Strub. A Formal Library for Elliptic Curves in the Coq Proof Assistant (Slides) |
|---|
| 11:15-11:45 | Kento Emoto, Frédéric Loulergue and Julien Tesson. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (Slides) |
|---|
| 11:45-12:15 | Peter Lammich. Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm (Slides) |
|---|
| 12:15-12:45 | Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel. Cardinals in Isabelle/HOL (Slides) |
|---|
| 12:45-13:00 | Rob Arthan. HOL Constant Definitions Done Right (Slides) |
|---|
| Session 36C 14:30-16:00 |
| 14:30-15:00 | Guyslain Naves and Arnaud Spiwack. Balancing lists: a proof pearl |
|---|
| 15:00-16:00 | Rod Chapman and Florian Schanda. Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK (Slides) |
|---|
| Session 38B 16:30-18:00 |
| 16:30-17:00 | Daniel Matichuk, Makarius Wenzel and Toby Murray. An Isabelle Proof Method Language (Slides) |
|---|
| 17:00-17:30 | Makarius Wenzel. Asynchronous User Interaction and Tool Integration in Isabelle/PIDE (Slides) |
|---|
| 17:30-18:00 | Martin Ring and Christoph Lüth. Collaborative Interactive Theorem Proving with Clide (Slides) |
|---|
| Wednesday, July 16th |
| Session 43C 10:45-13:00 |
| 10:45-11:15 | Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote and Enrico Tassi. A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) |
|---|
| 11:15-11:45 | Cyril Cohen and Anders Mörtberg. A Coq Formalization of Finitely Presented Modules (Slides) |
|---|
| 11:45-12:15 | Mohamed Yousri Mahmoud, Vincent Aravantinos and Sofiene Tahar. Formal Verification of Optical Quantum Flip Gate (Slides) |
|---|
| 12:15-12:45 | Umair Siddique, Mohamed Yousri Mahmoud and Sofiene Tahar. On the Formalization of Z-Transform in HOL |
|---|
| 12:45-13:00 | Disha Puri, Sandip Ray, Kecheng Hao and Fei Xie. Mechanical Certification of Loop Pipelining Transformations: A Preview (Slides) |
|---|
| Session 46C 14:30-16:00 |
| 14:30-15:00 | Timothy Bourke, Rob Van Glabbeek and Peter Höfner. Showing invariance compositionally for a process algebra of network protocols (Slides) |
|---|
| 15:00-16:00 | Peter Sewell. Retrofitting Rigour (Slides) |
|---|
| Session 48C 16:30-18:00 |
| 16:30-17:00 | Jeremy Avigad, Robert Y. Lewis and Cody Roux. A heuristic prover for real inequalities (Slides) |
|---|
| 17:00-17:30 | Tobias Nipkow and Dmitriy Traytel. Unified Decision Procedures for Regular Expression Equivalence (Slides) |
|---|
| 17:30-18:00 | Sandrine Blazy, Vincent Laporte and David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (Slides) |
|---|
| Thursday, July 17th |
| Session 54AC 10:45-13:00 |
| 10:45-11:15 | Robert Dockins. Formalized, effective domain theory in Coq (Slides) |
|---|
| 11:15-11:45 | Christian Doczkal and Gert Smolka. Completeness and Decidability Results for CTL in Coq (Slides) |
|---|
| 11:45-12:15 | Matthieu Sozeau and Nicolas Tabareau. Universe Polymorphism in Coq |
|---|
| 12:15-12:45 | Gregory Malecha, Adam Chlipala and Thomas Braibant. Compositional Computational Reflection |
|---|
| 12:45-13:00 | Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C semantics: CompCert and the C standard (Slides) |
|---|
| Session 62AC 14:30-16:00 |
| 14:30-15:00 | Nao Hirokawa, Aart Middeldorp and Christian Sternagel. A New and Formalized Proof of Abstract Completion |
|---|
| 15:00-15:30 | Jean-François Dufourd. Hypermap Specification and Certified Linked Implementation using Orbits (Slides) |
|---|
| 15:30-16:00 | Vincent Aravantinos and Sofiene Tahar. Implicational Rewriting Tactics in HOL (Slides) |
|---|
