11 citations · 24 across the 4 of their papers we have counts for
Showing 2015Show all
2 papers · 1 filter
cs.LO2015★ 4 cited
Mixing HOL and Coq in Dedukti (Extended Abstract)
Ali Assaf, Raphaël Cauderlier
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 pro…
cs.LO2015★ 11 cited
Checking Zenon Modulo Proofs in Dedukti
Raphaël Cauderlier, Pierre Halmagrand
Dedukti has been proposed as a universal proof checker. It is a logical framework based on the lambda Pi calculus modulo that is used as a backend to verify proofs coming from theo…