Proof mining with dependent types

Ekaterina Komendantskaya*, Jonathan Heras

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

5 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationIntelligent Computer Mathematics. CICM 2017.
EditorsH. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke
Number of pages16
ISBN (Electronic)978-3-319-62075-6
ISBN (Print)9783319620749
Publication statusE-pub ahead of print - 28 Jun 2017
Event10th International Conference on Intelligent Computer Mathematics - The University of Edinburgh, Edinburgh, United Kingdom
Duration: 17 Jul 201721 Jul 2017 (Conference website)

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference10th International Conference on Intelligent Computer Mathematics
Abbreviated titleCICM 2017
Country/TerritoryUnited Kingdom
OtherDigital 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


  • Clustering
  • Coq
  • Dependent types
  • Interactive theorem proving
  • Machine learning
  • Tactics
  • Theory exploration

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Proof mining with dependent types'. Together they form a unique fingerprint.

Cite this