Proof mining with dependent types

Ekaterina Komendantskaya, Jonathan Heras

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

5 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationIntelligent Computer Mathematics. CICM 2017.
EditorsH. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke
PublisherSpringer
Pages303-318
Number of pages16
Volume10383
ISBN (Electronic)978-3-319-62075-6
ISBN (Print)9783319620749
DOIs
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
http://www.cicm-conference.org/2017/cicm.php (Conference website)

Publication series

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

Conference

Conference10th International Conference on Intelligent Computer Mathematics
Abbreviated titleCICM 2017
CountryUnited Kingdom
CityEdinburgh
Period17/07/1721/07/17
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

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