23 citations · 49 across the 6 of their papers we have counts for
6 papers
Dedukti: a Logical Framework based on the -Calculus Modulo Theory
Ali Assaf, Guillaume Burel, Raphaël Cauderlier +7
Dedukti is a Logical Framework based on the -Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simpl…
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…
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…
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…
Completeness of algebraic CPS simulations
Ali Assaf, Simon Perdrix
The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independent…
Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
Ali Assaf, Alejandro Díaz-Caro, Simon Perdrix +2
We examine the relationship between the algebraic lambda-calculus, a fragment of the differential lambda-calculus and the linear-algebraic lambda-calculus, a candidate lambda-calcu…