Lieu de la réunion: Irif, Bâtiment Sophie Germain, Université Paris Cité, salle 3052.
Pour diminuer le nombre de concept que les étudiants doivent maitriser dans des experiences de preuves mathématiques concernant des nombres, nous suggérons une librairie introductive où le seul type de nombre utilisé est celui des nombres réels. Nous montrons comment quelques commandes peuvent être ajoutées pour ajouter aux nombres réels des fonctionalités qui sont habituellement fournies seulement pour les nombres naturels ou les nombres entiers.
L'overloading consiste à utiliser un même symbole pour représenter différentes fonctions, en comptant sur les types pour déterminer à quelle fonction il est fait référence. L'utilisation de l'overloading est omniprésente en mathématiques, et apparaît également dans certains langages de programmation. Ce travail propose le premier algorithme de typage visant à résoudre le problème général de la résolution statique de la surcharge dans les expressions mathématiques ainsi que dans les programmes bien typés. Cette année, avec Martin Bodin nous avons affiné les derniers détails de l'algorithme, complété l'implémentation du prototype, et aggrandi notre collection d'exemples.
Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of theorems, when such obvious replacements are typically left implicit on paper. This talk presents Trocq, a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Coq proof assistant, in the CoqElpi meta-language. We use this plugin on a gallery of representative examples of proof transfer issues in interactive theorem proving, and illustrate how Trocq covers the spectrum of several existing tools, used in program verification as well as in formalized mathematics in the broad sense.
Joint work with Enzo Crance and Assia Mahboubi
The jsCoq project enables users to embed Coq code and run Coq directly within a webpage, facilitating interactive formal documents using only a modern browser.
jsCoq began in 2015 as an experiment to test the js_of_ocaml compiler, later evolving to offer an install-free distribution of math-comp proofs in a convenient presentation format.
The combination of (a) an install-free Coq setup, (b) full-featured package manager with many contributions available, and (c) a literate programming format made jsCoq quite popular within the Coq teaching community.
However, the first jsCoq implementation had several limitations in terms of usability, document expressiveness, and constraints inherent to Coq’s standard document manager, the STM.
Work began in 2016 to replace the STM with a model better suited for jsCoq's rich document model and usability needs, culminating in 2022 with Flèche, a new document manager for Coq specifically designed to accommodate jsCoq use cases.
In this talk, we will introduce jsCoq 2, a major update to the jsCoq based on Flèche and the coq-lsp language server.
jsCoq 2 offers a continuous interaction model better suited for teaching and directly supports rich, jsCoq-style documents. This update addresses many technical challenges and enables users to develop courses and interactive documents entirely in the browser, using different editors, including rich WYSIWYG ones.
We will discuss the context and design requirements behind jsCoq and Flèche, providing a detailed overview of jsCoq 2's main features, novelties, and future roadmap.
jsCoq 2 is joint work with Shachar Itzhaky (Technion - Israel Institute of Technology).
Les structures canoniques telles qu'implémentées actuellement posent des problème de performance que l'on observe aujourd'hui lorsqu'il y a trop de structures emboîtées les unes dans les autres (e.g. https://github.com/math-comp/math-comp/pull/1125). Cela est dû à l'algorithme d'unification qui résoud de faux problèmes de structure canonique, au sens où il n'y a pas vraiment de structure à inférer. Je vais vous présenter dans les grandes lignes comment fonctionne l'algorithme d'unification de Coq/Rocq, puis la tentative actuelle de résolution de ce problème et ses conséquences.
Les preuves mathématiques sont souvent représentées de manière très graphique, et d'une manière assez différente de celle de Coq. Le but ici est de réfléchir à quoi pourrait ressembler Coq avec du graphisme, en restraignant le sujet au plus simple des objects graphiques : un tableau de variation. Je vais vous présenter les expériences que nous avons fait à Grenoble, ainsi que l'interface que nous proposons.
Réunion LiberAbaci Hosted by Yves Bertot https://inria.webex.com/inria-en/j.php?MTID=m69339f37f91b5cdeac642fc694ffd0ce Thursday, October 17, 2024 9:00 AM | 10 hours | (UTC+02:00) Brussels, Copenhagen, Madrid, Paris Occurs every day effective 10/17/2024 until 10/18/2024 from 9:00 AM to 7:00 PM, (UTC+02:00) Brussels, Copenhagen, Madrid, Paris Meeting number: 2740 262 2278 Password: maKYGhrP522 Join by video system Dial 27402622278@inria.webex.com You can also dial 62.109.219.4 and enter your meeting number. Join by phone +33-1-8514-8835 France Toll 2 Access code: 274 026 22278