| HAL-Inria | Publications, software ... of Inria's scientists |
Mixing HOL and Coq in Dedukti (Rough Diamond)
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.
Cited literature [9 references]
https://hal.inria.fr/hal-01141789
Contributor : Ali Assaf Connect 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
Contributor : Ali Assaf Connect 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
File
dedukti-interop.pdf
Files produced by the author(s)