List of accepted papers
List of accepted papers
David Monniaux and Pierre Corbineau.
On the Generation of Positivstellensatz Witnesses in Degenerate Cases
Anthony Fox.
LCF-style Bit-Blasting in HOL4
Johannes Hölzl and Armin Heller.
Three Chapters of Measure Theory in Isabelle/HOL
Andreas Lochbihler and Lukas Bulwahn.
Animating the Formalised Semantics of a Java-like Language
Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski and Lars Birkedal.
Verifying object-oriented programs with higher-order separation logic in Coq
Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs and Jürgen Giesl. Termination of Isabelle Functions via Termination of Rewriting
Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest and Marc Cavazza.
Structural Analysis of Narratives with the Coq Proof Assistant
Proving Valid Quantified Boolean Formulas in HOL Light
Relational decomposition
Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio and Jose-Luis Ruiz-Reina.
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments
Scott Owens, Peter Boehm, Francesco Zappa Nardelli and Peter Sewell.
Lightweight Tools for Heavyweight Semantics
Peter Reid and Ruben Gamboa.
Automatic Differentiation in ACL2
Magnus O. Myreen and Jared Davis.
A verified runtime for a verified theorem prover
Sylvain Heraud and David Nowak.
A Formalization of Polytime Functions
Chunhan Wu, Xingyuan Zhang and Christian Urban.
A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions (Proof Pearl)
Renaud Clavel, Laurence Pierre and Regis Leveugle.
Towards Robustness Analysis using PVS
Matej Urbas and Mateja Jamnik.
Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers
Phil Scott and Jacques Fleuriot.
Composable Discovery Engines for Interactive Theorem Proving
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
Point-free, set-free concrete linear alegbra
Tarek Mhamdi, Osman Hasan and Sofiene Tahar.
Formalization of Entropy Measures in HOL
Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein. seL4 Enforces Integrity
Ramana Kumar and Tjark Weber.
Validating QBF Validity in HOL4
Mechanised Computability Theory