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 proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publicationProgramming 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, Proceedings
EditorsHongseok Yang
PublisherSpringer/Verlag
Pages111-140
Number of pages30
ISBN (Print)9783662544334
DOIs
Publication statusPublished - 1 Jan 2017
Event26th 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 201729 Apr 2017

Publication series

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

Conference

Conference26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
CountrySweden
City Uppsala
Period22/04/1729/04/17

Fingerprint Dive into the research topics of 'Friends with benefits: Implementing corecursion in foundational proof assistants'. Together they form a unique fingerprint.

  • 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, 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