kth.sePublications KTH
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
Dep., Universitat de Barcelona, 100190, Barcelona, Spain.
Dep., Ifo Institute, 100190, Munich, Germany.
Univ. Bordeaux, Bordeaux INP, CNRS, UMR 5800 LaBRI, 33400, Talence, France.
Université Paris Cité, CNRS, Inria, IRIF, 75013, Paris, France.
Show others and affiliations
2025 (English)In: Journal of automated reasoning, ISSN 0168-7433, E-ISSN 1573-0670, Vol. 69, no 1, article id 8Article in journal (Refereed) Published
Abstract [en]

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

Place, publisher, year, edition, pages
Springer Nature , 2025. Vol. 69, no 1, article id 8
Keywords [en]
Community, Coq, Statistical analysis, Survey
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-360894DOI: 10.1007/s10817-025-09720-1ISI: 001427046000001Scopus ID: 2-s2.0-85218425845OAI: oai:DiVA.org:kth-360894DiVA, id: diva2:1942557
Note

QC 20250310

Available from: 2025-03-05 Created: 2025-03-05 Last updated: 2025-03-10Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Palmskog, Karl

Search in DiVA

By author/editor
Palmskog, Karl
By organisation
Theoretical Computer Science, TCS
In the same journal
Journal of automated reasoning
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 65 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf