Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. - Jasmin Christian Blanchette; Aymeric Bouzy; Andreas Lochbihler; Andrei Popescu 001; Dmitriy Traytel (ESOP, 2017)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)