Proof Mining with Dependent Types

被引：5

作者：

Komendantskaya, Ekaterina ^{[1
]}

Heras, Jonathan ^{[2
]}

机构：

[1] Heriot Watt Univ, Math & Comp Sci, Edinburgh, Midlothian, Scotland

[2] Univ La Rioja, Math & Comp Sci, Rioja, Spain

来源：

INTELLIGENT COMPUTER MATHEMATICS | 2017年 / 10383卷

基金：

英国工程与自然科学研究理事会;

关键词：

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

D O I：

10.1007/978-3-319-62075-6_21

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：303 / 318

页数：16

共 50 条

[31] Parametricity and Dependent Types
Bernardy, Jean-Philippe
Jansson, Patrik
Paterson, Ross
ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2010, : 345 - 356
[32] Games for Dependent Types
Abramsky, Samson
Jagadeesan, Radha
Vakar, Matthijs
AUTOMATA, LANGUAGES, AND PROGRAMMING, PT II, 2015, 9135 : 31 - 43
[33] Dependent Types at Work
Bove, Ana
Dybjer, Peter
LANGUAGE ENGINEERING AND RIGOROUS SOFTWARE DEVELOPMENT, 2009, 5520 : 57 - 99
[34] Parametricity and Dependent Types
Bernardy, Jean-Philippe
Jansson, Patrik
Paterson, Ross
ACM SIGPLAN NOTICES, 2010, 45 (09) : 345 - 356
[35] Dependent types for JavaScript
Chugh, Ravi
Herman, David
Jhala, Ranjit
ACM SIGPLAN Notices, 2012, 47 (10): : 587 - 606
[36] A shock-proof and ray-proof container for different types of roentgen tubes
Thoraeus, R
ACTA RADIOLOGICA, 1937, 18 (1/2) : 236 - 242
[37] Dependent Event Types
Luo, Zhaohui
Soloviev, Sergei
LOGICAL ASPECTS OF COMPUTATIONAL LINGUISTICS: CELEBRATING 20 YEARS OF LACL (1996-2016), 2016, 10054 : 333 - 334
[38] Dependent Event Types
Luo, Zhaohui
Soloviev, Sergei
LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION: 24TH INTERNATIONAL WORKSHOP, WOLLIC 2017, LONDON, UK, JULY 18-21, 2017, PROCEEDINGS, 2017, 10388 : 216 - 228
[39] Subtyping dependent types
Aspinall, D
Compagnoni, A
11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, : 86 - 97
[40] Defunctionalization with Dependent Types
Huang, Yulong
Yallop, Jeremy
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (PLDI):

← 1 2 3 4 5 →