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.
CITATION STYLE
Komendantskaya, E., & Heras, J. (2017). Proof mining with dependent types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10383 LNAI, pp. 303–318). Springer Verlag. https://doi.org/10.1007/978-3-319-62075-6_21
Mendeley helps you to discover research relevant for your work.