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 <>
Submitted on : Monday, April 13, 2015 - 5:13:32 PM
Last modification on : Thursday, March 5, 2020 - 6:49:51 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

256

Files downloads

126