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