23 citations · 49 across the 6 of their papers we have counts for
Showing 2015Show all
3 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★ 12 cited
Translating HOL to Dedukti
Ali Assaf, Guillaume Burel
Dedukti is a logical framework based on the lambda-Pi-calculus modulo rewriting, which extends the lambda-Pi-calculus with rewrite rules. In this paper, we show how to translate th…
cs.LO2015
Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version)
Ali Assaf
The lambda Pi calculus can be extended with rewrite rules to embed any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative…