Recycling Proof Patterns in Coq: Case Studies

Jonathan Heras (Lead / Corresponding author), Ekaterina Komendantskaya (Lead / Corresponding author)

    Research output: Contribution to journalArticle

    6 Citations (Scopus)

    Abstract

    Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophistication, the re-use of libraries by non-experts or across domains is a challenge. In this paper, we provide detailed case studies and evaluate the machine-learning tool ML4PG built to interactively data-mine the electronic libraries of proofs, and to provide user guidance on the basis of proof patterns found in the existing libraries.
    Original languageEnglish
    Pages (from-to)99-116
    Number of pages18
    JournalMathematics in Computer Science
    Volume8
    Issue number1
    DOIs
    Publication statusPublished - 2014

    Fingerprint Dive into the research topics of 'Recycling Proof Patterns in Coq: Case Studies'. Together they form a unique fingerprint.

  • Projects

    Cite this