Friends with Benefits

Jasmin Christian Blanchette (1, 2, 3) , Aymeric Bouzy (4) , Andreas Lochbihler (5) , Andrei Popescu (6) , Dmitriy Traytel (5)

1 MPII - Max-Planck-Institut für Informatik
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
3 MOSEL - Proof-oriented development of computer-based systems
4 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
5 ETH Zürich - Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich]
6 INFO - Département informatique

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.

Domaines: Logique en informatique [cs.LO]

Jasmin Christian 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⟩