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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-01401812
Contributor : Jasmin Christian Blanchette <>
Submitted on : Wednesday, November 23, 2016 - 5:48:49 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:27 PM
Document(s) archivé(s) le : Monday, March 20, 2017 - 7:05:05 PM

File

amico_abs.pdf
Files produced by the author(s)

Identifiers

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

Share

Metrics

Record views

391

Files downloads

116