kth.sePublikationer KTH
Driftstörningar
Det förekommer återkommande driftstörningar på några av sök-portalerna på grund av hög belastning. Vi arbetar på att lösa problemet, ni kan tillfälligt mötas av ett felmeddelande.
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • 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.
Visa övriga samt affilieringar
2025 (Engelska)Ingår i: Journal of automated reasoning, ISSN 0168-7433, E-ISSN 1573-0670, Vol. 69, nr 1, artikel-id 8Artikel i tidskrift (Refereegranskat) 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).

Ort, förlag, år, upplaga, sidor
Springer Nature , 2025. Vol. 69, nr 1, artikel-id 8
Nyckelord [en]
Community, Coq, Statistical analysis, Survey
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
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
Anmärkning

QC 20250310

Tillgänglig från: 2025-03-05 Skapad: 2025-03-05 Senast uppdaterad: 2025-03-10Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Person

Palmskog, Karl

Sök vidare i DiVA

Av författaren/redaktören
Palmskog, Karl
Av organisationen
Teoretisk datalogi, TCS
I samma tidskrift
Journal of automated reasoning
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 106 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf