Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download

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

File

dedukti-interop.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01141789, version 1

Collections

Citation

Ali Assaf, Raphaël Cauderlier. Mixing HOL and Coq in Dedukti (Rough Diamond). 2015. ⟨hal-01141789⟩

Share

Metrics

Record views

120

Files downloads

58