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

9 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 languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication26th 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
EditorsHongseok Yang
PublisherSpringer/Verlag
Pages111-140
Number of pages30
ISBN (Electronic)9783662544341
ISBN (Print)9783662544334
DOIs
Publication statusPublished - 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
Country/TerritorySweden
City Uppsala
Period22/04/1729/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.

FundersFunder number
Horizon 2020 Framework Programme713999
Engineering and Physical Sciences Research CouncilEP/N019547/1
European Research Council
Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung153217

    Fingerprint

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

    Cite this