Program

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

Comments are closed