Tuesday, July 23rd
8:30-8:50 Registration
8:50-9:00 Welcome from the chairs
9:00-10:00 Invited talk 1 - Chair: David Pichardie

Applying formal methods in the large
Dominique Bolignano
10:00-10:30 Break
10:30-12:00 Session 1: Regular Papers - Chair: Makarius Wenzel

MaSh: Machine Learning for Sledgehammer
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk and Josef Urban

Scalable LCF-style proof translation
Cezary Kaliszyk and Alexander Krauss

Lightweight proof by reflection using a posteriori simulation of effectful computation
Guillaume Claret, Lourdes Del Carmen Gonzalez Huesca, Yann Regis-Gianas and Beta Ziliani
12:00-13:45 Lunch
13:45-14:30 Session 2: Rough Diamonds - Chair: Yves Bertot

Communicating Formal Proofs: The Case of Flyspeck
Carst Tankink, Cezary Kaliszyk, Josef Urban and Herman Geuvers

Square Root and Division Elimination in PVS
Pierre Neron

The Picard Algorithm for Ordinary Differential Equations in Coq
Evgeny Makarov and Bas Spitters
14:30-16:00 Session 3: Regular Papers - Chair: Michael Norrish

Data Refinement in Isabelle/HOL
Florian Haftmann, Alexander Krauss, Ondrej Kuncar and Tobias Nipkow

Automatic Data Refinement
Peter Lammich

Light-weight containers for Isabelle: efficient, extensible, nestable
Andreas Lochbihler
16:00-16:30 Break
16:30-17:30 Tutorial 1 - Chair: Laurence Pierre

Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities
Pete Manolios
18:00-19:30 Townhall Reception
Wednesday, July 24th
8:30-9:00 Registration
9:00-10:00 Invited talk 2 - Chair: Christine Paulin-Mohring

Automating theorem proving with SMT
Rustan Leino
10:00-10:30 Break
10:30-12:00 Session 4: Regular Papers - Chair: Larry Paulson

Ordinals in HOL: Transfinite Arithmetic up to (and beyond) omega
Michael Norrish and Brian Huffman

Mechanising Turing Machines and Computability Theory in Isabelle/HOL
Jian Xu, Xingyuan Zhang and Christian Urban

A Machine-Checked Proof of the Odd Order Theorem
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi and Laurent Thery
12:00-13:45 Lunch
13:45-14:30 Session 5: Rough Diamonds - Chair: Assia Mahboubi

Stateless Higher-Order Logic with Quantified Type
Evan Austin and Perry Alexander

Implementing hash-consed data structures in Coq
Thomas Braibant, Jacques-Henri Jourdan and David Monniaux

Towards Certifying Network Calculus
Etienne Mabille, Marc Boyer, Loïc Fejoz and Stephan Merz
14:30-16:00 Session 6: Regular Papers - Chair: Gerwin Klein

Kleene Algebra with Tests and Coq Tools for While Programs
Damien Pous

Program Verification based on Kleene Algebra in Isabelle/HOL
Alasdair Armstrong, Georg Struth and Tjark Weber

Pragmatic Quotient Types in Coq
Cyril Cohen
16:00-16:30 Break
16:30-18:00 Tutorial 2 - Chair: Pete Manolios

The Mathematical Components library: principles and design choices
Assia Mahboubi and Enrico Tassi
18:00-18:30 Business Meeting
Thursday, July 25th
8:30-9:00 Registration
9:00-10:30 Session 7: Regular Papers - Chair: Stephan Merz

Mechanical Verification of SAT Refutations with Extended Resolution
Nathan Wetzler, Marijn Heule and Warren Hunt Jr

Formalizing Bounded Increase
René Thiemann

Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
Mark Bickford, Vincent Rahli and Abhishek Anand
10:30-11:00 Break
11:00-12:30 Session 8: Regular Papers - Chair: Tobias Nipkow

Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
Johannes Hölzl, Fabian Immler and Brian Huffman

Formal Reasoning about Classified Markov Chains in HOL
Liya Liu, Osman Hasan, Vincent Aravantinos and Sofiene Tahar

Practical Probability: Applying pGCL to Lattice Scheduling
David Cock
12:30-14:15 Lunch
14:15-23:00 Social Event: Mont Saint-Michel

Guided tour of the village and the abbey OR walking trip into the bay at low tide

Conference dinner
Friday, July 26th
8:30-9:00 Registration
9:00-10:00 Invited talk 3 - Chair: Sandrine Blazy

Certifying voting protocols
Carsten Schürmann
10:00-10:30 Break
10:30-12:00 Session 9: Regular Papers - Chair: Xavier Leroy

Adjustable references
Viktor Vafeiadis

Handcrafted Inversions Made Operational on Operational Semantics
Jean-François Monin and Xiaomu Shi

Circular Coinduction in Coq using Bisimulation-Up-To Techniques
Joerg Endrullis, Dimitri Hendriks and Martin Bodin
12:00-13:45 Lunch
13:45-14:00 Session 10: Rough Diamond - Chair: Guillaume Melquiond

Steps Towards Verified Implementations of HOL Light
Magnus O. Myreen, Scott Owens and Ramana Kumar
14:00-15:30 Session 11: Regular Papers - Chair: Guillaume Melquiond

Program Extraction from Nested Definitions
Kenji Miyamoto, Fredrik Nordvall Forsberg and Helmut Schwichtenberg

Subformula Linking as an Interaction Method
Kaustuv Chaudhuri

Automatically generated infrastructure for De Bruijn syntaxes
Emmanuel Polonowski
15:30-16:00 Break
16:00-17:00 Session 12: Regular Papers - Chair: Magnus Myreen

Shared-Memory Multiprocessing for Interactive Theorem Proving
Makarius Wenzel

A Parallelized Theorem Prover for a Logic with Parallel Execution
David L Rager, Warren A. Jr. Hunt and Matt Kaufmann
17:00 Closing Remarks