David Delahaye, Catherine Dubois, Jean-Frédéric Étienne. Extracting Purely Functional Contents from Logical Inductive Types. In Klaus Schneider, Jens Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings. Volume 4732 of Lecture Notes in Computer Science, pages 70-85, Springer, 2007. [doi]
Abstract is missing.