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'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.
Type de document :
Communication dans un congrès
Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Apr 2017, Uppsala, Sweden
Liste complète des métadonnées

Littérature citée [70 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01599167
Contributeur : Jasmin Christian Blanchette <>
Soumis le : dimanche 1 octobre 2017 - 18:34:47
Dernière modification le : lundi 20 novembre 2017 - 15:14:02

Fichier

conf.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01599167, version 1

Citation

Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel. Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants. Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Apr 2017, Uppsala, Sweden. 〈hal-01599167〉

Partager

Métriques

Consultations de la notice

99

Téléchargements de fichiers

10