10 citations · 18 across the 10 of their papers we have counts for
4 papers · 1 filter
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families
Catherine Dubois, Nicolas Magaud, Alain Giorgetti
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are ver…
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving
Catherine Dubois, Bruno Woltzenlogel Paleo
This volume of EPTCS contains the proceedings of the Fifth Workshop on Proof Exchange for Theorem Proving (PxTP 2017), held on September 23-24, 2017 as part of the Tableaux, FroCoS…
Tableaux Modulo Theories Using Superdeduction
Mélanie Jacquel, Karim Berkani, David Delahaye +1
We propose a method that allows us to develop tableaux modulo theories using the principles of superdeduction, among which the theory is used to enrich the deduction system with ne…
Why Would You Trust B?
Eric Jaeger, Catherine Dubois
The use of formal methods provides confidence in the correctness of developments. Yet one may argue about the actual level of confidence obtained when the method itself -- or its i…