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

A first look at an emerging model of community organizations for the long-term maintenance of ecosystems' packages

Autor: Théo Zimmermann

Publikováno v: SoHeal 2020-3rd International Workshop on Software Health
SoHeal 2020-3rd International Workshop on Software Health, May 2020, Seoul, South Korea. ⟨10.1145/3387940.3392209⟩
ICSE (Workshops)
SoHeal 2020-3rd International Workshop on Software Health, May 2020, Seoul / Virtual, South Korea. ⟨10.1145/3387940.3392209⟩

One of the biggest strength of many modern programming languages is their rich open source package ecosystem. Indeed, modern language-specific package managers have made it much easier to share reusable code and depend on components written by someon

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0ab00e2df35badbf7a4b092c045806a6
http://arxiv.org/abs/2004.03347

Impact of Switching Bug Trackers: A Case Study on a Medium-Sized Open Source Project

Autor: Annali Casanueva Artis, Théo Zimmermann

Publikováno v: ICSME
ICSME 2019-International Conference on Software Maintenance and Evolution
ICSME 2019-International Conference on Software Maintenance and Evolution, Sep 2019, Cleveland, United States
HAL

International audience; For most software projects, the bug tracker is an essential tool. In open source development, this tool plays an even more central role as it is generally open to all users, who are encouraged to test the software and report b

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6f3ed831cad4de66c8d026bc0b064d23
https://doi.org/10.1109/icsme.2019.00011

Coq's Prolog and application to defining semi-automatic tactics

Autor: Théo Zimmermann, Hugo Herbelin

Publikováno v: Type Theory Based Tools
Type Theory Based Tools, Jan 2017, Paris, France
HAL

International audience; We report on a work-in-progress to re-implement Coq's apply tactic in order to embed some form of simple automation. We design it in a declarative way, relying on typeclasses eauto, a tactic which gives access to the proof-sea

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

BBCA: Improving the scalability of *BEAST using random binning

Autor: Siavash Mirarab, Théo Zimmermann, Tandy Warnow

Publikováno v: BMC Genomics

Background Species tree estimation can be challenging in the presence of gene tree conflict due to incomplete lineage sorting (ILS), which can occur when the time between speciation events is short relative to the population size. Of the many methods

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::893914ac6f488c1f60c9100ce89148b7
https://pubmed.ncbi.nlm.nih.gov/25572469