Recycling Proof Patterns in Coq: Case Studies

Jonathan Heras; Ekaterina Komendantskaya

doi:10.1007/s11786-014-0173-1

Recycling Proof Patterns in Coq: Case Studies

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

Research output: Contribution to journal › Article › peer-review

9 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 language	English
Pages (from-to)	99-116
Number of pages	18
Journal	Mathematics in Computer Science
Volume	8
Issue number	1
DOIs	https://doi.org/10.1007/s11786-014-0173-1
Publication status	Published - 2014

Access to Document

10.1007/s11786-014-0173-1

Cite this

@article{510d62a33a3747f38d3b58fe51f73073,

title = "Recycling Proof Patterns in Coq: Case Studies",

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.",

author = "Jonathan Heras and Ekaterina Komendantskaya",

year = "2014",

doi = "10.1007/s11786-014-0173-1",

language = "English",

volume = "8",

pages = "99--116",

journal = "Mathematics in Computer Science",

issn = "1661-8270",

publisher = "Springer Verlag",

number = "1",

}

TY - JOUR

T1 - Recycling Proof Patterns in Coq

T2 - Case Studies

AU - Heras, Jonathan

AU - Komendantskaya, Ekaterina

PY - 2014

Y1 - 2014

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

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

UR - http://www.scopus.com/inward/record.url?scp=84901244669&partnerID=8YFLogxK

U2 - 10.1007/s11786-014-0173-1

DO - 10.1007/s11786-014-0173-1

M3 - Article

AN - SCOPUS:84901244669

SN - 1661-8270

VL - 8

SP - 99

EP - 116

JO - Mathematics in Computer Science

JF - Mathematics in Computer Science

IS - 1

ER -

Recycling Proof Patterns in Coq: Case Studies

Abstract

Access to Document

Other files and links

Fingerprint

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)

Cite this

Recycling Proof Patterns in Coq: Case Studies

Abstract

Access to Document

Other files and links

Fingerprint

Projects

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)

Cite this