Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
In: Leibniz International Proceedings in Informatics ; 14th International Conference on Interactive Theorem Proving (ITP 2023) ; https://telecom-paris.hal.science/hal-04098856 ; 14th International Conference on Interactive Theorem Proving (ITP 2023), Jul 2023, Białystok, Poland. pp.1-18, ⟨10.4230/LIPIcs.ITP.2023.12⟩ ; https://mizar.uwb.edu.pl/ITP2023/, 2023
Online
Konferenz
Zugriff:
International audience ; The Coq Community Survey 2022 was an online public survey of users of the Coq proof assistant conducted during February 2022. Broadly, the survey asked about use of Coq features, user interfaces, libraries, plugins, and tools, views on renaming Coq and Coq improvements, and also demographic data such as education and experience with Coq and other proof assistants and programming languages. The survey received 466 submitted responses, making it the largest survey of users of an interactive theorem prover (ITP) so far. We present the design of the survey, a summary of key results, and analysis of answers relevant to ITP technology development and usage. In particular, we analyze user characteristics associated with adoption of tools and libraries and make comparisons to adjacent software communities. Notably, we find that experience has significant impact on Coq user behavior, including on usage of tools, libraries, and integrated development environments.
| Titel: |
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
|
|---|---|
| Autor/in / Beteiligte Person: | de Almeida Borges, Ana ; Artís, Annalí, Casanueva ; Falleri, Jean-Rémy ; Gallego Arias, Emilio Jesús ; Martin-Dorel, Érik ; Palmskog, Karl ; Serebrenik, Alexander ; Zimmermann, Théo ; University of Barcelona ; Institute, Ifo ; Laboratoire Bordelais de Recherche en Informatique (LaBRI) ; Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS) ; Institut Universitaire de France (IUF) ; Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (M.E.N.E.S.R.) ; Les assistants à la démonstration au cœur du raisonnement mathématique (PICUBE) ; Inria de Paris ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-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é) ; Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE) ; Institut de recherche en informatique de Toulouse (IRIT) ; Université Toulouse Capitole (UT Capitole) ; Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J) ; Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3) ; Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP) ; Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI) ; Université Toulouse - Jean Jaurès (UT2J) ; Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3) ; Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole) ; Université de Toulouse (UT) ; Université Toulouse III - Paul Sabatier (UT3) ; KTH Royal Institute of Technology Stockholm (KTH ) ; Eindhoven University of Technology Eindhoven (TU/e) ; Autonomic and Critical Embedded Systems (ACES) ; Laboratoire Traitement et Communication de l'Information (LTCI) ; Institut Mines-Télécom Paris (IMT)-Télécom Paris-Institut Mines-Télécom Paris (IMT)-Télécom Paris ; Département Informatique et Réseaux (INFRES) ; ParisTech, Télécom ; Naumowicz, Adam ; Thiemann, René |
| Link: | |
| Zeitschrift: | Leibniz International Proceedings in Informatics ; 14th International Conference on Interactive Theorem Proving (ITP 2023) ; https://telecom-paris.hal.science/hal-04098856 ; 14th International Conference on Interactive Theorem Proving (ITP 2023), Jul 2023, Białystok, Poland. pp.1-18, ⟨10.4230/LIPIcs.ITP.2023.12⟩ ; https://mizar.uwb.edu.pl/ITP2023/, 2023 |
| Veröffentlichung: | HAL CCSD ; Dagstuhl Publishing, 2023 |
| Medientyp: | Konferenz |
| DOI: | 10.4230/LIPIcs.ITP.2023.12 |
| Schlagwort: |
|
| Sonstiges: |
|