Recycling proof patterns in Coq: case studies
From MaRDI portal
Publication:475385
DOI10.1007/S11786-014-0173-1zbMATH Open1302.68243arXiv1301.6039OpenAlexW2071091648MaRDI QIDQ475385FDOQ475385
Authors: Jónathan Heras, Ekaterina Komendantskaya 
Publication date: 26 November 2014
Published in: Mathematics in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1301.6039
Recommendations
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Matita interactive theorem prover
- Types for Proofs and Programs
- Pattern recognition and machine learning.
- A constructive approach to sequential Nash equilibria
- Isabelle/HOL. A proof assistant for higher-order logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- An introduction to small scale reflection in Coq
- Formal proof - the four color theorem
- Learning Boolean functions in an infinite attribute space
- Proof-Pattern Recognition and Lemma Discovery in ACL2
- Type classes for efficient exact real arithmetic in Coq
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Conjecture synthesis for inductive theories
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
- Recycling proof patterns in Coq: case studies
- A Machine-Checked Proof of the Odd Order Theorem
- A verified information-flow architecture
Cited In (7)
- JEFL: joint embedding of formal proof libraries
- Aligning concepts across proof assistant libraries
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- TacticToe: learning to prove with tactics
- Deepalgebra -- an outline of a program
- Proof mining with dependent types
- Recycling proof patterns in Coq: case studies
Uses Software
This page was built for publication: Recycling proof patterns in Coq: case studies
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q475385)
