10 citations · 18 across the 3 of their papers we have counts for
3 papers
cs.LO2021★ 8 cited
A modular construction of type theories
Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger +2
The lambda-Pi-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several…
cs.LO2021
Encoding of Predicate Subtyping with Proof Irrelevance in the -Calculus Modulo Theory
Gabriel Hondet, Frédéric Blanqui
The -calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof…
cs.PL2020★ 10 cited
The New Rewriting Engine of Dedukti
Gabriel Hondet, Frédéric Blanqui
Dedukti is a type-checker for the -calculus modulo rewriting, an extension of Edinburgh's logicalframework LF where functions and type symbols can be defined by rewrite rules…