Proof assistants are tools allowing to formally express mathematical statements and their proofs, and to mechanically check their correctness. At their core, they consist of a logical system materialized by a formal symbolic language for expressing statements and proofs, together with an algorithm deciding the validity of such proofs. These components are called the Kernel of such tools, and they are the basis for the trust in the theorems that one proves using a proof assistant. As such, kernels enjoy of the most scrutiny and meta-theoretical focus. However, the logical langage of a kernel is too excplicit and inconvenient to manipulate and to read. For this reason, the langage that is exposed to a proof assistant’s user is a high level one, which is then elaborated to the kernels language. In this talk, I will present (in the context of the Rocq proof assistant) two major parts of elaboration: generalized dependent pattern matching and higher-order unification. I will discuss how they contribute to the expressivity of the user-level language, and challenges that arise in implementing them and in formalizing them.
Localisation
Salle de séminaire 4B107 (bâtiment Copernic)
5, boulevard Descartes, 77420 Champs-sur-Marne