| Monday 22 August 2016 | |
|---|---|
| 08:00–08:50 | Registration |
| 08:50–09:00 | Welcome from the program chairs |
| Session 1 (chair: Stephan Merz) | |
| 09:00–10:00 | Invited talk: Propositions as Programs, Proofs as Programs (slides) Viktor Kuncak |
| 10:00–10:30 | Visual theorem proving with the Incredible Proof Machine (slides) Joachim Breitner |
| 10:30–11:00 | Break |
| Session 2 (chair: Michael Norrish) | |
| 11:00–11:30 | HOL Zero’s Solutions for Pollack-Inconsistency Mark Adams |
| 11:30–12:00 | From Types to Sets by Local Type Definitions in Higher-Order Logic Ondřej Kunčar, Andrei Popescu |
| 12:00–12:30 | CoqPIE: An IDE aimed at improving proof development productivity (rough diamond) (slides, video) Ken Roe, Scott Smith |
| 12:30–14:00 | Lunch |
| Session 3 (chair: Andrei Popescu) | |
| 14:00–14:30 | Modular dependent induction in Coq, Mendler-style (slides) Paolo Torrini |
| 14:30–15:00 | Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms (slides) Thomas Grégoire, Adam Chlipala |
| 15:00–15:30 | Equational Reasoning with Applicative Functors (slides) Andreas Lochbihler, Joshua Schneider |
| 15:30–16:00 | Break |
| Session 4 (chair: Christian Urban) | |
| 16:00–16:30 | A Formal Proof of Cauchy’s Residue Theorem (slides) Wenda Li, Lawrence C. Paulson |
| 16:30–17:00 | What’s in a Theorem Name? (rough diamond) David Aspinall, Cezary Kaliszyk |
| 17:00–17:30 | On the Formalization of Fourier Transform in Higher-order Logic (rough diamond) (slides) Adnan Rashid, Osman Hasan |
| 19:00– | Cocktail reception |
| Tuesday 23 August 2016 | |
| Session 5 (chair: Lawrence Paulson) | |
| 09:00–10:00 | Invited talk: Dijkstra monads for free: A framework for deriving and extending F*’s effectful semantics (slides) Nikhil Swamy |
| 10:00–10:30 | Algebraic Numbers in Isabelle/HOL (slides) René Thiemann, Akihisa Yamada |
| 10:30–11:00 | Break |
| Session 6 (chair: Jørgen Villadsen) | |
| 11:00–11:30 | Formally Verified Approximations of Definite Integrals Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote |
| 11:30–12:00 | The Flow of ODEs (slides) Fabian Immler, Christoph Traut |
| 12:00–12:30 | Bounding Least Common Multiples with Triangles (proof pearl) (slides) Hing Lun Chan, Michael Norrish |
| 12:30–14:00 | Lunch |
| Session 7 (chair: Viktor Kuncak) | |
| 14:00–14:30 | AUTO2, a saturation-based heuristic prover for higher-order logic (slides) Bohua Zhan |
| 14:30–15:00 | Automatic Functional Correctness Proofs for Functional Search Trees Tobias Nipkow |
| 15:00–15:30 | Cardinalities of Relations in Coq (rough diamond) Paul Brunet, Damien Pous, Insa Stucke |
| 15:30–16:00 | Break |
| Session 8 (chair: René Thiemann) | |
| 16:00–16:30 | Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems (slides) Julian Nagele, Aart Middeldorp |
| 16:30–17:00 | Proof of OS scheduling behavior in the presence of interrupt-induced concurrency (slides) June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah |
| 17:00–17:30 | POSIX Lexing with Derivatives of Regular Expressions (proof pearl) Fahad Ausaf, Roy Dyckhoff, Christian Urban |
| Wednesday 24 August 2016 | |
| Session 9 (chair: Andreas Lochbihler) | |
| 09:00–09:30 | Formalizing the Edmonds-Karp Algorithm (slides) Peter Lammich, S. Reza Sefidgar |
| 09:30–10:00 | Two-Way Automata in Coq (slides) Christian Doczkal, Gert Smolka |
| 10:00–10:30 | Formalized Timed Automata (slides) Simon Wimmer |
| 10:30–11:00 | Break |
| Session 10 (chair: Grant Olney Passmore) | |
| 11:00–11:30 | Infeasible paths elimination by symbolic execution techniques: Proof of monotonicity and correctness (slides) Romain Aïssat, Frédéric Voisin, Burkhart Wolff |
| 11:30–12:00 | Verified operational transformation for trees (slides) Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov |
| 12:00–12:30 | A Framework for the Automatic Formal Verification of Refinement from Cogent to C (slides) Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O’Connor, Toby Murray, Gabriele Keller, Gerwin Klein |
| 12:30–14:00 | Lunch |
| Session 11 (chair: Christian Doczkal) | |
| 14:00–14:30 | Formalization of the Resolution Calculus for First-Order Logic (slides) Anders Schlichtkrull |
| 14:30–15:00 | Hereditarily Finite Sets in Constructive Type Theory (slides) Gert Smolka, Kathrin Stark |
| 15:00–15:30 | Mechanical Verification of a Constructive Proof for FLP (slides) Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann |
| 15:30–16:15 | Business meeting |
| 17:30–19:00 | Guided tour of Nancy |
| 19:30– | Conference dinner |
| Thursday 25 August 2016 | |
| Session 12 (chair: Jasmin Blanchette) | |
| 09:00–10:00 | Invited talk: Formal Verification of Financial Algorithms, Progress and Prospects Grant Olney Passmore |
| 10:00–10:30 | CoSMed: A Confidentiality-Verified Social Media Platform (slides) Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi |
| 10:30–11:00 | Break |
| Session 13 (chair: June Andronick) | |
| 11:00–11:30 | An Isabelle/HOL Formalisation of Green’s Theorem (slides) Mohammad Abdulaziz, Lawrence C. Paulson |
| 11:30–12:00 | Formalizing Semantics for Expected Running Time of Probabilistic Programs (rough diamond) (slides) Johannes Hölzl |
| 12:00–12:15 | Our Experience with CoCon |
| 12:15–12:30 | ITP 2017 in Brasília |
| 12:30–14:00 | Lunch |
