Proof mining with dependent types

  1. Komendantskaya, E. 1
  2. Heras, J. 2
  1. 1 Heriot-Watt University
    info

    Heriot-Watt University

    Edimburgo, Reino Unido

    ROR https://ror.org/04mghma93

  2. 2 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Año de publicación: 2017

Volumen: 10383 LNAI

Páginas: 303-318

Tipo: Artículo

DOI: 10.1007/978-3-319-62075-6_21 SCOPUS: 2-s2.0-85025155806 GOOGLE SCHOLAR

Otras publicaciones en: Lecture Notes in Computer Science

Resumen

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. © Springer International Publishing AG 2017.