Abstract
Several approaches exist to datamining 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 simplytyped 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.
Original language  English 

Title of host publication  Intelligent Computer Mathematics. CICM 2017. 
Editors  H. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke 
Publisher  Springer 
Pages  303318 
Number of pages  16 
Volume  10383 
ISBN (Electronic)  9783319620756 
ISBN (Print)  9783319620749 
DOIs  
Publication status  Epub ahead of print  28 Jun 2017 
Event  10th International Conference on Intelligent Computer Mathematics  The University of Edinburgh, Edinburgh, United Kingdom Duration: 17 Jul 2017 → 21 Jul 2017 http://www.cicmconference.org/2017/cicm.php (Conference website) 
Publication series
Name  Lecture Notes in Computer Science 

Volume  10383 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Conference
Conference  10th International Conference on Intelligent Computer Mathematics 

Abbreviated title  CICM 2017 
Country  United Kingdom 
City  Edinburgh 
Period  17/07/17 → 21/07/17 
Other  Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. The Conference on Intelligent Computer Mathematics (CICM) offers a venue for discussing and developing solutions to the great challenges posed by the integration of these diverse areas. 
Internet address 

Keywords
 Clustering
 Coq
 Dependent types
 Interactive theorem proving
 Machine learning
 Tactics
 Theory exploration
ASJC Scopus subject areas
 Theoretical Computer Science
 Computer Science(all)
Fingerprint Dive into the research topics of 'Proof mining with dependent types'. Together they form a unique fingerprint.
Cite this
Komendantskaya, E., & Heras, J. (2017). Proof mining with dependent types. In H. Geuvers, M. England, O. Hasan, F. Rabe, & O. Teschke (Eds.), Intelligent Computer Mathematics. CICM 2017. (Vol. 10383, pp. 303318). (Lecture Notes in Computer Science; Vol. 10383). Springer. https://doi.org/10.1007/9783319620756_21