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

Publikováno v: 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

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

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::87a5249b64e406f647afa438650c1b13
https://hal.archives-ouvertes.fr/hal-03404668/document