Mixing HOL and Coq in Dedukti (Extended Abstract)

Ali Assaf
(Inria, Ecole Polytechnique)
Raphaël Cauderlier
(Inria, CNAM)

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. We illustrate our approach with a concrete example where we instantiate a sorting algorithm written in Coq with the natural numbers of HOL.

In Cezary Kaliszyk and Andrei Paskevich: Proceedings Fourth Workshop on Proof eXchange for Theorem Proving (PxTP 2015), Berlin, Germany, August 2-3, 2015, Electronic Proceedings in Theoretical Computer Science 186, pp. 89–96.
Published: 30th July 2015.

ArXived at: https://dx.doi.org/10.4204/EPTCS.186.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org