Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment

Autor: Pierre Castéran, Jérémy Damour, Karl Palmskog, Clément Pit-Claudel, Théo Zimmermann
Přispěvatelé: Université de Bordeaux (UB), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université Sciences et Technologies - Bordeaux 1-Université Bordeaux Segalen - Bordeaux 2, Université de Paris - UFR Médecine [Santé] (UP Médecine Paris Centre), Université de Paris (UP), Royal Institute of Technology [Stockholm] (KTH ), MIT Computer Science & Artificial Intelligence Lab (MIT CSAIL), Massachusetts Institute of Technology (MIT), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Design, study and implementation of languages for proofs and programs (PI.R2), Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Paris (UP)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP)-Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Paris Cité (UPCité)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)
Jazyk: angličtina
Rok vydání: 2021
Předmět:
Zdroj: Journées Francophones des Langages Applicatifs: JFLA 2022
Journées Francophones des Langages Applicatifs: JFLA 2022, Feb 2022, St-Médard d'Excideuil, France
HAL
Journées Francophones des Langages Applicatifs: JFLA 2022, Jun 2022, St-Médard d'Excideuil, France
Popis: International audience; Hydras & Co. is a collaborative library of discrete mathematics for the Coq proof assistant, developed as part of the Coq-community organization on GitHub. The Coq code is accompanied by an electronic book, generated with the help of the Alectryon literate proving tool. We present the evolution of the mathematical contents of the library since former presentations at JFLA meetings. Then, we describe how the structure of the project is determined by two requirements which must be continuously satisfied. First, the Coq code needs to be compatible with its ever-evolving dependencies (the Coq proof assistant and several Coq packages both from inside and outside Coq-community) and reverse dependencies (Coq-community projects that depend on it). Second, the book needs to be consistent with the Coq code, which undergoes frequent changes to improve structure and include new material. We believe Hydras & Co. demonstrates that books on formalized mathematics are not limited to providing exposition of theories and reasoning techniquesthey can also provide inspiration and entertainment that transcends educational goals.
Databáze: OpenAIRE
Externí odkaz: