Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving.

Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette

Browse the full LICS paper archive.