Regular Papers
Wenda Li, Lawrence C. Paulson. A Formal Proof of Cauchy’s Residue Theorem
Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O’Connor, Toby Murray, Gabriele Keller, Gerwin Klein. A Framework for the Automatic Formal Verification of Refinement from Cogent to C
Bohua Zhan. AUTO2, a saturation-based heuristic prover for higher-order logic
René Thiemann, Akihisa Yamada. Algebraic Numbers in Isabelle/HOL
Mohammad Abdulaziz, Lawrence C. Paulson. An Isabelle/HOL Formalisation of Green’s Theorem
Tobias Nipkow. Automatic Functional Correctness Proofs for Functional Search Trees
Julian Nagele and Aart Middeldorp. Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi. CoSMed: A Confidentiality-Verified Social Media Platform
Andreas Lochbihler, Joshua Schneider. Equational Reasoning with Applicative Functors
Anders Schlichtkrull. Formalization of the Resolution Calculus for First-Order Logic
Simon Wimmer. Formalized Timed Automata
Peter Lammich, S. Reza Sefidgar. Formalizing the Edmonds-Karp Algorithm
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals
Ondřej Kunčar, Andrei Popescu. From Types to Sets by Local Type Definitions in Higher-Order Logic
Mark Adams. HOL Zero’s Solutions for Pollack-Inconsistency
Gert Smolka, Kathrin Stark. Hereditarily Finite Sets in Constructive Type Theory
Romain Aïssat, Frédéric Voisin, Burkhart Wolff. Infeasible paths elimination by symbolic execution techniques: proof of monotonicity and correctness
Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann. Mechanical Verification of a Constructive Proof for FLP
Paolo Torrini. Modular dependent induction in Coq, Mendler-style
Thomas Grégoire, Adam Chlipala. Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah. Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
Fabian Immler, Christoph Traut. The Flow of ODEs
Christian Doczkal, Gert Smolka. Two-Way Automata in Coq
Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov. Verified operational transformation for trees
Joachim Breitner. Visual theorem proving with the Incredible Proof Machine
Proof Pearls
Hing Lun Chan, Michael Norrish. Bounding Least Common Multiples with Triangles
Fahad Ausaf, Roy Dyckhoff, Christian Urban. POSIX Lexing with Derivatives of Regular Expressions
Rough Diamonds
Paul Brunet, Damien Pous, Insa Stucke. Cardinalities of Relations in Coq
Ken Roe, Scott Smith. CoqPIE: An IDE aimed at improving proof development productivity
Johannes Hölzl. Formalizing Semantics for Expected Running Time of Probabilistic Programs
Adnan Rashid, Osman Hasan. On the Formalization of Fourier Transform in Higher-order Logic
David Aspinall, Cezary Kaliszyk. What’s in a Theorem Name?
