ABSTRACT. TBA

ABSTRACT. We present a small Coq library for collecting side conditions and deferring their proof.

ABSTRACT. In this talk we present an ongoing effort to develop a Coq formal library about elementary real analysis, in a firmly classical setting. Almost all existing proof assistants on the market have been used to define real numbers, and to investigate the formalization of real, and sometimes also complex, analysis. A survey by Boldo et al. reviews the different approaches and the breadth of the existing developments. In particular, the Coq standard library provides an axiomatization of real numbers, with a classical flavor and the Coquelicot external library is a conservative extension thereof. At the time of writing, these libraries however cover far less material that their analogues in the HOL ecosystem, including Harrison’s HOL Light library and its translation to Isabelle/HOL.

The present work is yet another attempt at providing a library for classical analysis in Coq. The motivation is twofold. First, the library relies on stronger classical axioms, so as to get closer to the logical formalism used in classical mathematics. In particular, this impacts the formalization of compactness-related facts. Second, the library is designed along the formalization methodology put into practice in the Mathematical Components libraries. The latter libraries are essentially geared towards algebra and this work aims at providing an extension for topics in analysis. However, we incorporated a significant subset of the Coquelicot library. The main original contributions lie in the effort put in the infrastructure of the library: automation, notations, etc. The library is still rather incomplete, but it proved already useful enough for a few applications.

ABSTRACT. I propose a talk to open a discussion about this topic. My extended abstract details the motivation and the context. Briefly, oracles are a key ingredient in the success of CompCert. Such an oracle is an untrusted foreign code which outputs are checked by certified code. However, in CompCert, oracles are currently invoked through an unsafe FFI. I will illustrate some pitfalls of this FFI and propose how to overcome them. Moreover, I will conjecture that by using an adequate FFI, we can derive ``theorems for free'' a la Wadler in Coq from the Ocaml type of polymorphic oracles, and thus discharge a part of the certification on the Ocaml typechecker. However, my proposal raises more issues than it solves: in other words, it opens a new topic of research.

ABSTRACT. Yet Another deep embedding of Linear Logic in Coq

We present some results and comments around the ongoing development of the Yalla library which provides a deep embedding of linear logic in Coq relying on an explicit exchange rule.

ABSTRACT. TBA

ABSTRACT. We present a Coq plugin for performing completion procedures on rewriting rules given by users. The result is added in a hint rewrite database which works with an automated rewriting tactic, so it enables us to write proof scripts more simply.

ABSTRACT. We present a translation of guarded recursive functions in Coq to well-founded recursive functions using only case analysis eliminators and the eliminator of the accesibility predicate. This work-in-progress is a possible first step towards a formalization of Coq's guard condition. We also present an idea to extend the guard recursion to handle inductive-inductive definitions.

ABSTRACT. Coq's notation system is both extremely powerful and confusingly ad-hoc. While powerful enough to pretty-print abstract syntax trees in most domain-specific languages, how to do so does not seem to be common knowledge. Typical questions arising from such an endeavor might include "How do I pick notation levels?", "Why are these notations clashing?", "Which things should be marked as symbols?", "How do I use boxes in `format`?", and "How do I get parentheses to show up (only) where I want them to?" This interactive presentation aims to serve as a guide to these questions and more, by demonstrating and explaining how to pretty-print subsets of C using only Coq's `Notation` mechanism.

ABSTRACT. We present some early work being done to utilize Artificial Intelligence for proof search in the Coq theorem prover. In a similar vein as the TacticToe project for HOL4, we are working on a system that finds proofs of goals on the tactic level, by learning from previous tactic scripts. Learning on the level of tactics has several advantages over more low-level approaches. First, this allows for much coarser proof steps, meaning that during proof search more complicated proofs can be found. Second, it allows for the usage of custom built, domain specific tactics that where previously defined and used in the development. This will allow for better performance of the system in very specialized domains. The rest of this abstract will describe the required components of our system. Since a number of technical issues need to be addressed, we hope to solicit feedback from the Coq developers at the workshop.