Mathieu Boespflug, Guillaume Burel. CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo. In David Pichardie, Tjark Weber, editors, Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012. Volume 878 of CEUR Workshop Proceedings, pages 44-50, CEUR-WS.org, 2012. [doi]
Abstract is missing.