Andreas Schropp, Andrei Popescu 0001. Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. In Georges Gonthier, Michael Norrish, editors, Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Volume 8307 of Lecture Notes in Computer Science, pages 114-130, Springer, 2013. [doi]
Abstract is missing.