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


Ondřej Kunčar.

Proving Valid Quantified Boolean Formulas in HOL Light


Lennart Beringer.

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


Peter Gammie.

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


Tobias Nipkow.

Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism


Georges Gonthier.

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


Michael Norrish.

Mechanised Computability Theory