Abstract : We use Dedukti as a logical framework for interoperability. We use automated tools to translate different developments made in HOL and in Coq to Dedukti and we combine them to prove new results.
https://hal.inria.fr/hal-01141789 Contributor : Ali AssafConnect in order to contact the contributor Submitted on : Monday, April 13, 2015 - 5:13:32 PM Last modification on : Friday, August 5, 2022 - 2:54:00 PM Long-term archiving on: : Tuesday, April 18, 2017 - 5:52:18 PM