Auto in agda programming proof search using reflection

Wen Kokke; Wouter Swierstra

doi:10.1007/978-3-319-19797-5_14

Auto in agda programming proof search using reflection

Wen Kokke, Wouter Swierstra

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.

Original language	English
Title of host publication	Mathematics of Program Construction
Subtitle of host publication	12th International Conference, Königswinter, Germany, June 29--July 1, MPC 2015, Proceedings
Editors	Janis Voigtländer, Ralf Hinze
Publisher	Springer-Verlag
Pages	276-301
Number of pages	26
Volume	9129
ISBN (Electronic)	9783319197968
DOIs	https://doi.org/10.1007/978-3-319-19797-5_14
Publication status	Accepted/In press - 16 Mar 2015
Externally published	Yes
Event	12th International Conference on Mathematics of Program Construction - Konigswinter, Germany Duration: 29 Jun 2015 → 1 Jul 2015 Conference number: 12 http://www.cs.ox.ac.uk/conferences/MPC2015/

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9129
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th International Conference on Mathematics of Program Construction
Abbreviated title	MPC 2015
Country/Territory	Germany
City	Konigswinter
Period	29/06/15 → 1/07/15
Internet address	http://www.cs.ox.ac.uk/conferences/MPC2015/

Access to Document

10.1007/978-3-319-19797-5_14

Auto in Agda_KOKKE_DoA160315_AFVAccepted author manuscript, 378 KB

https://www.springer.com/gp/book/9783319197968Licence: All Rights Reserved

Cite this

Kokke, W., & Swierstra, W. (Accepted/In press). Auto in agda programming proof search using reflection. In J. Voigtländer, & R. Hinze (Eds.), Mathematics of Program Construction : 12th International Conference, Königswinter, Germany, June 29--July 1, MPC 2015, Proceedings (Vol. 9129, pp. 276-301). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9129). Springer-Verlag. https://doi.org/10.1007/978-3-319-19797-5_14

Kokke, Wen ; Swierstra, Wouter. / Auto in agda programming proof search using reflection. Mathematics of Program Construction : 12th International Conference, Königswinter, Germany, June 29--July 1, MPC 2015, Proceedings. editor / Janis Voigtländer ; Ralf Hinze. Vol. 9129 Springer-Verlag, 2015. pp. 276-301 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{bf0b089bb0e94e03bc83e065505bcc77,

title = "Auto in agda programming proof search using reflection",

abstract = "As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda{\textquoteright}s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.",

author = "Wen Kokke and Wouter Swierstra",

year = "2015",

month = mar,

day = "16",

doi = "10.1007/978-3-319-19797-5_14",

language = "English",

volume = "9129",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag",

pages = "276--301",

editor = "Janis Voigtl{\"a}nder and Ralf Hinze",

booktitle = "Mathematics of Program Construction",

note = "12th International Conference on Mathematics of Program Construction , MPC 2015 ; Conference date: 29-06-2015 Through 01-07-2015",

url = "http://www.cs.ox.ac.uk/conferences/MPC2015/",

}

Kokke, W & Swierstra, W 2015, Auto in agda programming proof search using reflection. in J Voigtländer & R Hinze (eds), Mathematics of Program Construction : 12th International Conference, Königswinter, Germany, June 29--July 1, MPC 2015, Proceedings. vol. 9129, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9129, Springer-Verlag, pp. 276-301, 12th International Conference on Mathematics of Program Construction , Konigswinter, Germany, 29/06/15. https://doi.org/10.1007/978-3-319-19797-5_14

Auto in agda programming proof search using reflection. / Kokke, Wen; Swierstra, Wouter.
Mathematics of Program Construction : 12th International Conference, Königswinter, Germany, June 29--July 1, MPC 2015, Proceedings. ed. / Janis Voigtländer; Ralf Hinze. Vol. 9129 Springer-Verlag, 2015. p. 276-301 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9129).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Auto in agda programming proof search using reflection

AU - Kokke, Wen

AU - Swierstra, Wouter

N1 - Conference code: 12

PY - 2015/3/16

Y1 - 2015/3/16

N2 - As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.

AB - As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.

UR - http://www.scopus.com/inward/record.url?scp=84937501475&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-19797-5_14

DO - 10.1007/978-3-319-19797-5_14

M3 - Conference contribution

AN - SCOPUS:84937501475

VL - 9129

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 276

EP - 301

BT - Mathematics of Program Construction

A2 - Voigtländer, Janis

A2 - Hinze, Ralf

PB - Springer-Verlag

T2 - 12th International Conference on Mathematics of Program Construction

Y2 - 29 June 2015 through 1 July 2015

ER -

Kokke W, Swierstra W. Auto in agda programming proof search using reflection. In Voigtländer J, Hinze R, editors, Mathematics of Program Construction : 12th International Conference, Königswinter, Germany, June 29--July 1, MPC 2015, Proceedings. Vol. 9129. Springer-Verlag. 2015. p. 276-301. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-19797-5_14

Auto in agda programming proof search using reflection

Abstract / Description of output

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this