Proof Mining with Dependent Types

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.

Accepted at CICM'17, Edinburgh, 17-21 July 2017

References in corpus (3)

• SEPIA: Search for Proofs Using Inferred Automata
• Hipster: Integrating Theory Exploration in a Proof Assistant
• Mining State-Based Models from Proof Corpora

Cited by in corpus (1)

• Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)