65 citations · 211 across the 36 of their papers we have counts for
42 papers
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Melanie Taprogge, Frédéric Blanqui, Alexander Steen
We identify common challenges and requirements for verifying proofs from automated theorem provers in the Dedukti logical framework and develop a general methodology for deriving e…
Sharing proofs with predicative theories through universe-polymorphic elaboration
Thiago Felicissimo, Frédéric Blanqui
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the…
Translating proofs from an impredicative type system to a predicative one
Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the…
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…
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…
Type safety of rewrite rules in dependent types
Frédéric Blanqui
The expressiveness of dependent type theory can be extended by identifying types modulo some additional computation rules. But, for preserving the decidability of type-checking or…