Lessons for Interactive Theorem Proving Researchers from a Survey of Coq UsersLessons for Interactive Theorem Proving Researchers from a...A. de Almeida Borges et al.

被引：0

作者：

Ana de Almeida Borges ^{[1
]}

Annalí Casanueva Artís ^{[2
]}

Jean-Rémy Falleri ^{[3
]}

Emilio Jesús Gallego Arias ^{[4
]}

Érik Martin-Dorel ^{[5
]}

Karl Palmskog ^{[6
]}

Alexander Serebrenik ^{[7
]}

Théo Zimmermann ^{[8
]}

机构：

[1] Dep.,Department of Computer Science

[2] Universitat de Barcelona,Mathematics and Computer Science

[3] Dep.,undefined

[4] Ifo Institute,undefined

[5] Univ. Bordeaux,undefined

[6] Bordeaux INP,undefined

[7] CNRS,undefined

[8] UMR 5800 LaBRI,undefined

[9] Université Paris Cité,undefined

[10] CNRS,undefined

[11] Inria,undefined

[12] IRIF,undefined

[13] Dep.,undefined

[14] IRIT,undefined

[15] CNRS,undefined

[16] Toulouse INP,undefined

[17] Université de Toulouse,undefined

[18] KTH Royal Institute of Technology,undefined

[19] Eindhoven University of Technology,undefined

[20] LTCI,undefined

[21] Télécom Paris,undefined

[22] Institut Polytechnique de Paris,undefined

来源：

Journal of Automated Reasoning | 2025年 / 69卷 / 1期

关键词：

Coq; Community; Survey; Statistical analysis;

D O I：

10.1007/s10817-025-09720-1

中图分类号：

学科分类号：

摘要：

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 (IDEs).

引用

共 3 条

[1] Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
Borges, Ana de Almeida
Artis, Annali Casanueva
Falleri, Jean-Remy
Gallego Arias, Emilio Jesus
Martin-Dorel, Erik
Palmskog, Karl
Serebrenik, Alexander
Zimmermann, Theo
JOURNAL OF AUTOMATED REASONING, 2025, 69 (01)
[2] Preface: Selected Extended Papers from Interactive Theorem Proving 2018
Avigad, Jeremy
Mahboubi, Assia
JOURNAL OF AUTOMATED REASONING, 2020, 64 (05) : 793 - 794
[3] Preface: Selected Extended Papers from Interactive Theorem Proving 2018
Jeremy Avigad
Assia Mahboubi
Journal of Automated Reasoning, 2020, 64 : 793 - 794

← 1 →