ITP on Wednesday, July 14th

09:00‑10:00 ITP Invited Talk
Chair: Christian Urban
Location: AT LT5
09:00 Benjamin C. Pierce (University of Pennsylvania)
Proof Assistants as Teaching Assistants: A View from the Trenches

Ambitious experiments using proof assistants for programming language research and teaching are all the rage. In this talk, I'll report on one now underway at the University of Pennsylvania and several other places: a one-semester graduate course in the theory of programming languages presented entirely---every lecture, every homework assignment---in Coq. This course is now in its third iteration, the course materials are becoming fairly mature, and we've got quite a bit of experience with what works and what doesn't. I'll try to give a sense of what the course is like for both instructors and students, describe some of the most interesting challenges, and explain why I now believe such machine-assisted courses are the way of the future.

10:30‑12:30 Session 8
Chair: Thorsten Altenkirch
Location: AT LT5
10:30 Matthieu Sozeau
Equations: a dependent pattern-matching compiler

We present a compiler for definitions made by pattern matching on inductive families in the Coq system. It allows to write structured, recursive dependently-typed functions, automatically find their realization in the core type theory and generate proofs to ease reasoning on them.

The basic functionality is the ability to define a function by a set of equations with patterns on the left-hand side and programs on the right-hand side, in a similar fashion to Haskell function definitions. The system also supports with-clauses (as in Epigram or Agda) that can be used to add patterns on the left-hand side for further refinement. Both "syntactic" structural recursion and "semantic" well-founded recursion schemes are available in definitions, the later being generalized enough to cope with general inductive families efficiently.

The system provides proofs of the equations that can be used as rewrite rules to simplify calls to the function. It also automatically generates the inductive graph of the function and a proof that the function respects it, giving a useful elimination principle for it. It provides a complete package to define and reason on functions in the proof assistant, substantially reducing the boilerplate code and proofs one usually has to write, also hiding the intricacies related to the use of dependent types and complex recursion schemes.

Elaboration into the core Coq type theory provides the smallest trusted code base possible and gives room for extensions at the user-level. The compiler makes heavy use of type classes and the high-level tactic language of Coq for greater genericity and extensibility.

11:00 Arthur Charguéraud
The Optimal Fixed Point Combinator

In this paper, we develop a general theory of fixed point combinators, in higher-order logic equipped with Hilbert's epsilon operator. This combinator allows for a direct and effective formalization of corecursive values, recursive and corecursive functions, as well as functions mixing recursion and corecursion. It supports higher-order recursion, nested recursion, and offers a proper treatment of partial functions in the sense that domains need not be hardwired in the definition of functionals. Our work, which has been entirely implemented in Coq, unifies and generalizes existing results on contraction conditions and complete ordered families of equivalences, and relies on the theory of optimal fixed points for the treatment of partial functions. It provides a practical way to formalize circular definitions in higher-order logic.

11:30 Thomas Braibant and Damien Pous
An Efficient Coq Tactic for Deciding Kleene Algebras

We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations almost instantaneously. The corresponding decision procedure was proved correct and complete; correctness is established w.r.t. any model (including binary relations), by formalising Kozen's initiality theorem.

12:00 Peter Lammich and Andreas Lochbihler
The Isabelle Collections Framework

The Isabelle Collections Framework (ICF) provides a unified framework for using verified collection data structures in Isabelle/HOL formalizations and generating efficient functional code in ML, Haskell, and OCaml. Thanks to its modularity, it is easily extensible and supports switching to different data structures any time. For good integration with applications, a data refinement approach separates the correctness proofs from implementation details. The generated code based on the ICF lies in better complexity classes than the one that uses Isabelle's default setup (logarithmic vs. linear time). In a case study with tree automata, we demonstrate that the ICF is easy to use and efficient: An ICF based, verified tree automata library outperforms the unverified Timbuk/Taml library by a factor of 14.

14:00‑15:00 Session 9
Chair: Jose Luis Ruiz-Reina
Location: AT LT5
14:00 Jasmin Christian Blanchette and Tobias Nipkow
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally a finite model finder, it approximates infinite types by finite subsets. As case studies, we consider a security type system and a hotel key card system. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick generates more counterexamples than other model finders for higher-order logic, without restrictions on the form of the formulas to falsify.

14:30 Alexander Krauss and Andreas Schropp
A Mechanized Translation from Higher-Order Logic to Set Theory

In order to make existing formalizations available for set-theoretic developments, we present an automated translation of theories from Isabelle/HOL to Isabelle/ZF. This covers all fundamental primitives, particularly type classes. The translation produces LCF-style theorems that are checked by Isabelle's inference kernel. Type checking is replaced by explicit reasoning about set membership.

15:30‑17:00 Session 10
Chair: Elsa Gunter
Location: AT LT5
15:30 Chantal Keller and Benjamin Werner
Importing HOL-Light into Coq

We present a new scheme to translate mathematical developments from HOL-light to Coq, where they can be re-used and re-checked. By relying on a carefully chosen embedding of Higher-Order Logic into Type Theory, we try to avoid some pitfalls of inter-operation between proof systems. In particular, our translation keeps the mathematical statements intelligible. This translation has been implemented and allows the importation of the HOL-light basic library into Coq.

16:00 Sascha Böhme and Tjark Weber
Fast LCF-Style Proof Reconstruction for Z3

The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs of unsatisfiability. We present independent checking of these proofs in the theorem provers Isabelle/HOL and HOL4, and in particular focus on the question of efficiency. Our highly optimized implementations outperform previous LCF-style proof checkers for SMT, often by orders of magnitude. Detailed performance data shows that LCF-style proof reconstruction can be faster than proof search in Z3.

16:30 Tjark Weber
Validating QBF Invalidity in HOL4

The Quantified Boolean Formulae (QBF) solver Squolem can generate certificates of invalidity, based on Q-resolution. We present independent checking of these certificates in the HOL4 theorem prover. This enables HOL4 users to benefit from Squolem's automation for QBF problems, and provides high correctness assurances for Squolem's results. Detailed performance data shows that LCF-style certificate checking is feasible even for large QBF instances. Our work prompted improvements to HOL4's inference kernel.