Friends with benefits: Implementing corecursion in foundational proof assistants

Jasmin Christian Blanchette; Aymeric Bouzy; Andreas Lochbihler; Andrei Popescu; Dmitriy Traytel

doi:10.1007/978-3-662-54434-1_5

Friends with benefits: Implementing corecursion in foundational proof assistants

Jasmin Christian Blanchette^*, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel

^*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

11 Downloads (Pure)

Abstract

We introduce AmiCo, a tool that extends a proof assistant, Isabelle/HOL, with flexible function definitions well beyond primitive corecursion. All definitions are certified by the assistant’s inference kernel to guard against inconsistencies. A central notion is that of friends: functions that preserve the productivity of their arguments and that are allowed in corecursive call contexts. As new friends are registered, corecursion benefits by becoming more expressive. We describe this process and its implementation, from the user’s specification to the synthesis of a higher-order definition to the registration of a friend. We show some substantial case studies where our approach makes a difference.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings
Editors	Hongseok Yang
Publisher	Springer/Verlag
Pages	111-140
Number of pages	30
ISBN (Electronic)	9783662544341
ISBN (Print)	9783662544334
DOIs	https://doi.org/10.1007/978-3-662-54434-1_5
Publication status	Published - 2017
Event	26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 - Uppsala, Sweden Duration: 22 Apr 2017 → 29 Apr 2017

Publication series

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

Conference

Conference	26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Country/Territory	Sweden
City	Uppsala
Period	22/04/17 → 29/04/17

Funding

Martin Desharnais spent months extending Isabelle?s codatatype command to generate a wealth of theorems, many of which were useful when implementing AmiCo. Lorenz Panny developed primcorec, whose code provided valuable building blocks. Mathias Fleury, Mark Summerfield, Daniel Wand, and the anonymous reviewers suggested many textual improvements. We thank them all. Blanchette is supported by the European Research Council (ERC) starting grant Matryoshka (713999). Lochbihler is supported by the Swiss National Science Foundation (SNSF) grant ?Formalising Computational Soundness for Protocol Implementations? (153217). Popescu is supported by the UK Engineering and Physical Sciences Research Council (EPSRC) starting grant ?VOWS: Verification of Web-based Systems? (EP/N019547/1). The authors are listed in alphabetical order.

Funders	Funder number
Horizon 2020 Framework Programme	713999
Engineering and Physical Sciences Research Council	EP/N019547/1
European Research Council
Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung	153217

Access to Document

10.1007/978-3-662-54434-1_5

Friends with benefits_Implementing corecursion in foundational proof assistantsFinal published version, 402 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

Blanchette, J. C., Bouzy, A., Lochbihler, A., Popescu, A., & Traytel, D. (2017). Friends with benefits: Implementing corecursion in foundational proof assistants. In H. Yang (Ed.), Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings (pp. 111-140). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10201 LNCS). Springer/Verlag. https://doi.org/10.1007/978-3-662-54434-1_5

Blanchette, Jasmin Christian ; Bouzy, Aymeric ; Lochbihler, Andreas et al. / Friends with benefits : Implementing corecursion in foundational proof assistants. Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings. editor / Hongseok Yang. Springer/Verlag, 2017. pp. 111-140 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9a41b92521f04bfa8bb9b313b06e558a,

title = "Friends with benefits: Implementing corecursion in foundational proof assistants",

abstract = "We introduce AmiCo, a tool that extends a proof assistant, Isabelle/HOL, with flexible function definitions well beyond primitive corecursion. All definitions are certified by the assistant{\textquoteright}s inference kernel to guard against inconsistencies. A central notion is that of friends: functions that preserve the productivity of their arguments and that are allowed in corecursive call contexts. As new friends are registered, corecursion benefits by becoming more expressive. We describe this process and its implementation, from the user{\textquoteright}s specification to the synthesis of a higher-order definition to the registration of a friend. We show some substantial case studies where our approach makes a difference.",

author = "Blanchette, {Jasmin Christian} and Aymeric Bouzy and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel",

year = "2017",

doi = "10.1007/978-3-662-54434-1_5",

language = "English",

isbn = "9783662544334",

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

publisher = "Springer/Verlag",

pages = "111--140",

editor = "Hongseok Yang",

booktitle = "Programming Languages and Systems",

note = "26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 ; Conference date: 22-04-2017 Through 29-04-2017",

}

Blanchette, JC, Bouzy, A, Lochbihler, A, Popescu, A & Traytel, D 2017, Friends with benefits: Implementing corecursion in foundational proof assistants. in H Yang (ed.), Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10201 LNCS, Springer/Verlag, pp. 111-140, 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, 22/04/17. https://doi.org/10.1007/978-3-662-54434-1_5

Friends with benefits: Implementing corecursion in foundational proof assistants. / Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas et al.
Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings. ed. / Hongseok Yang. Springer/Verlag, 2017. p. 111-140 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10201 LNCS).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Friends with benefits

T2 - 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017

AU - Blanchette, Jasmin Christian

AU - Bouzy, Aymeric

AU - Lochbihler, Andreas

AU - Popescu, Andrei

AU - Traytel, Dmitriy

PY - 2017

Y1 - 2017

N2 - We introduce AmiCo, a tool that extends a proof assistant, Isabelle/HOL, with flexible function definitions well beyond primitive corecursion. All definitions are certified by the assistant’s inference kernel to guard against inconsistencies. A central notion is that of friends: functions that preserve the productivity of their arguments and that are allowed in corecursive call contexts. As new friends are registered, corecursion benefits by becoming more expressive. We describe this process and its implementation, from the user’s specification to the synthesis of a higher-order definition to the registration of a friend. We show some substantial case studies where our approach makes a difference.

AB - We introduce AmiCo, a tool that extends a proof assistant, Isabelle/HOL, with flexible function definitions well beyond primitive corecursion. All definitions are certified by the assistant’s inference kernel to guard against inconsistencies. A central notion is that of friends: functions that preserve the productivity of their arguments and that are allowed in corecursive call contexts. As new friends are registered, corecursion benefits by becoming more expressive. We describe this process and its implementation, from the user’s specification to the synthesis of a higher-order definition to the registration of a friend. We show some substantial case studies where our approach makes a difference.

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

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

U2 - 10.1007/978-3-662-54434-1_5

DO - 10.1007/978-3-662-54434-1_5

M3 - Conference contribution

AN - SCOPUS:85018662884

SN - 9783662544334

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

SP - 111

EP - 140

BT - Programming Languages and Systems

A2 - Yang, Hongseok

PB - Springer/Verlag

Y2 - 22 April 2017 through 29 April 2017

ER -

Blanchette JC, Bouzy A, Lochbihler A, Popescu A, Traytel D. Friends with benefits: Implementing corecursion in foundational proof assistants. In Yang H, editor, Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings. Springer/Verlag. 2017. p. 111-140. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2017 Mar 19. doi: 10.1007/978-3-662-54434-1_5

Friends with benefits: Implementing corecursion in foundational proof assistants

Abstract

Publication series

Conference

Funding

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this