Back to Search Start Over

Proof Mining with Dependent Types

Authors :
Komendantskaya, Ekaterina
Heras, Jonathan
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

Details

Database :
arXiv
Publication Type :
Report
Accession number :
edsarx.1705.04680
Document Type :
Working Paper