ABSTRACT. Coq 8.5 has a number of new features. It has more powerful universe polymorphism support. It allows tactics to be run at interpretation to construct other terms. The ability to switch from Gallina to Ltac in arbitrary locations nicely complements the constr: notation permitting the switch from Ltac to Gallina in tactics, and opens up many new possibilities. I propose to present three tricks involving these new features: tactics in terms allows the construction of tactics that recurse under binders; tactics in terms together with typeclasses allows overloading notations based on the type of their arguments; and there is a way to talk about universe levels explicitly, helped along by tactics in terms.

ABSTRACT. The unification algorithm is at the heart of a proof assistant like Coq. In particular, it is a key component in the refiner (the algorithm who has to fill implicit terms and missing type annotations), and the application of lemmas. Despite of being so important, however, the current unification algorithm of Coq is not properly documented, and implements certain heuristics that makes unification hard to understand and unpredictable. In this talk we are going to present a new unification algorithm, built from scratch, which focuses on it being simple, easy to understand, sound, and configurable to adapt to the different needs.

ABSTRACT. We introduce various enhancements of the generalized rewriting system of Coq. First, we show how the framework can be lifted to proof-relevant relations using the newly introduced universe polymorphic definitions in Coq. Second, we introduce rewriting strategies as a monadic combinator library on top of this framework, ressembling the LogicT monad for proof-search (i.e., with backtracking, well-behaved choice and composition). These new features combine to provide a general tool for fine-tuned automated rewriting applicable not only to propositional relations but also general computational type-valued relations. Last, we will also present an idea to handle dependent rewriting, e.g. the ability to rewrite in the domain of a dependent product and get corresponding transportation obligations.

ABSTRACT. The Coq proof assistant is based on Martin-Loef's constructive type theory, as realized in the Calculus of Inductive Constructions.  Some recent mathematical models have provided a new perspective on constructive type theory, answering some fundamental questions, and suggesting certain new principles that can be added, such as higher inductive types and Voevodsky's univalence axiom.  In this talk, I will give a gentle introduction to homotopy type theory, and explain what impact it may have on developing proofs and programs in Coq.  Some questions that will be answered include: How is the logic of "homotopy propositions" different from the logic of Prop in CiC? What are univalence and higher inductive types, and what can they be used for? What changes have already been made to Coq to support homotopy type theory, and what might you expect in the future?  

ABSTRACT. Co-designing software or hardware systems and their formal proofs is an appealing idea, with the expectation that the rigor enforced by formal methods will percolate the whole design. In practice however, carrying out formal proofs while designing even a relatively simple system can be an exercise in frustration, with a great deal of time spent attempting to prove things about broken definitions, and countless iterations for discovering the correct lemmas and strengthening inductive invariants. We believe that property-based testing (PBT) can dramatically decrease the number of failed proof attempts and reduce the overall cost of producing formally verified systems. Despite the existence of experimental tools, Coq is still lagging behind proof assistants like Isabelle, which provides several mature PBT tools. We aim to improve the PBT support in Coq, while also investigating several innovations we could add into the mix like polarized mutation testing and a language-based approach to custom generation. We are also exploring whether PBT could bring more confidence to the implementation of Coq itself.

ABSTRACT. ML4PG is an extension of the Proof General interface of Coq, allowing the user to invoke machine-learning algorithms and find proof similarities in Coq/SSReflect libraries. In this talk, we will show the recent ML4PG features in action, using examples from the standard SSReflect library and HoTT library. We will compare ML4PG with traditional Coq searching tools and dependency graphs.

ABSTRACT. By adding redundant information to transmitted data, error-correcting codes (ECCs) make it possible to communicate reliably over noisy channels. Minimizing redundancy and coding/decoding time has driven much research, culminating with Low-Density Parity-Check (LDPC) codes. Hard-disk storage, wifi communications, mobile phones, etc.: most modern devices now rely on ECCs and in particular LDPC codes. Yet, correctness guarantees are only provided by research papers of ever-growing complexity. One solution to improve this situation is to provide a formalization of ECCs. We think that a first difficulty to achieve this goal has been lifted by the SSReflect library, that provides a substantial formalization of linear algebra. Using this library, we have been tackling the formalization of linear ECCs. Our formalization of linear ECCs is already rich enough to formalize most properties of Hamming codes and we are now in a position to formalize the more difficult LDPC codes.

ABSTRACT. Formalizing syntactic theories with variable binders is not easy. We present Autosubst, a library for the Coq proof assistant to automate this process. Given an inductive definition of syntactic objects in de Bruijn representation augmented with binding annotations, Autosubst synthesizes the parallel substitution operation and automatically proves the basic lemmas about substitutions. Our core contribution is an automation tactic that solves equations involving terms and substitutions. This makes the usage of substitution lemmas unnecessary. The tactic is based on our current work on a decision procedure for the equational theory of an extension of the sigma-calculus by Abadi et. al. The library is completely written in Coq and uses Ltac to synthesize the substitution operation.

ABSTRACT. We present the results of our efforts building compositional proof automation for program verification. We focus our efforts on abstract axiomatizations of different logics in order to make our procedures more generally applicable. Our automation leverages computational reflection to solve both intuitionistic and separation logic entailments. These specialized procedures are parameterized by auxiliary procedures that can reason about domain-specific theories such as arithmetic.

ABSTRACT. In this talk I will discuss the new jEdit editor integration for Coq, that supports asynchronous interaction with the proof assistant.

ABSTRACT. Users of modern IDEs expect sophisticated features like automatic dependency resolution, background recompilation, content-aware search features (such as "show me where this is defined"), automatic indentation, syntax highlighting and code completion. Coqoon, which is built on top of the Eclipse platform, provides such an IDE for Coq.