Friends with Benefits: Implementing Foundational Corecursion in Proof Assistants

Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel


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.

Extended Abstract