Friends with Benefits: Implementing Foundational Corecursion in Isabelle/HOL (Extended Abstract)

Abstract : We describe AmiCo, a tool that extends 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 may occur in corecursive call contexts. As new friends are registered , corecursion benefits by becoming more expressive.
Type de document :
Communication dans un congrès
Isabelle Workshop 2016, Aug 2016, Nancy, France
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01401812
Contributeur : Jasmin Christian Blanchette <>
Soumis le : mercredi 23 novembre 2016 - 17:48:49
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : lundi 20 mars 2017 - 19:05:05

Fichier

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

Identifiants

  • HAL Id : hal-01401812, version 1

Citation

Jasmin Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel. Friends with Benefits: Implementing Foundational Corecursion in Isabelle/HOL (Extended Abstract). Isabelle Workshop 2016, Aug 2016, Nancy, France. 〈hal-01401812〉

Partager

Métriques

Consultations de la notice

211

Téléchargements de fichiers

60