Back to Search
Start Over
Proof Mining with Dependent Types
- Publication Year :
- 2017
-
Abstract
- Several approaches exist to data-mining big corpora of formal proofs. Some of these approaches are based on statistical machine learning, and some -- on theory exploration. However, most are developed for either untyped or simply-typed theorem provers. In this paper, we present a method that combines statistical data mining and theory exploration in order to analyse and automate proofs in dependently typed language of Coq.<br />Comment: Accepted at CICM'17, Edinburgh, 17-21 July 2017
- Subjects :
- Computer Science - Programming Languages
Subjects
Details
- Database :
- arXiv
- Publication Type :
- Report
- Accession number :
- edsarx.1705.04680
- Document Type :
- Working Paper