Friends with benefits: implementing corecursion in foundational proof assistants

Conference paper

Blanchette, J., Bouzy, A., Lochbihler, A., Popescu, A. and Traytel, D. 2017. Friends with benefits: implementing corecursion in foundational proof assistants. 26th European Symposium on Programming, ESOP 2017. Uppsala, Sweden 22 - 29 Apr 2017 Springer. https://doi.org/10.1007/978-3-662-54434-1_5
TypeConference paper
TitleFriends with benefits: implementing corecursion in foundational proof assistants
AuthorsBlanchette, J., Bouzy, A., Lochbihler, A., Popescu, A. and Traytel, D.
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.

Research GroupFoundations of Computing group
Conference26th European Symposium on Programming, ESOP 2017
ISSN0302-9743
ISBN
Hardcover9783662544334
PublisherSpringer
Publication dates
Online19 Mar 2017
Publication process dates
Deposited19 Jun 2017
Accepted01 Feb 2017
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-54434-1_5

Additional information

Paper published as: Blanchette J.C., Bouzy A., Lochbihler A., Popescu A., Traytel D. (2017) Friends with Benefits. In: Yang H. (eds) Programming Languages and Systems. ESOP 2017. Lecture Notes in Computer Science, vol 10201. Springer, Berlin, Heidelberg

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-662-54434-1_5
LanguageEnglish
Book titleProgramming Languages and Systems. ESOP 2017. Lecture Notes in Computer Science, vol 10201
Permalink -

https://repository.mdx.ac.uk/item/870vx

Log in to edit

Download files

Accepted author manuscript
amicoupdate.pdf

  • 28
    total views
  • 6
    total downloads
  • 4
    views this month
  • 1
    downloads this month

Export as