The B-Book, Assigning Programs to Meanings, pp.10-1017, 1996. ,
Lambda calculus with types, pp.10-1017, 2013. ,
DOI : 10.1017/CBO9781139032636
Autarkic Computations in Formal Proofs, Journal of Automated Reasoning (JAR), vol.28, p.1015761529444, 2002. ,
Boogie: A modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects, pp.10-1007, 2006. ,
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism, Conference on Automated Deduction (CADE), 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00825086
CoqInE: translating the calculus of inductive constructions into the ??-calculus modulo, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-01126128
The ??-Calculus Modulo as a Universal Proof Language, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00917845
Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, LPAR), 2007. ,
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920
Experimenting with Deduction Modulo, Conference on Automated Deduction (CADE), LNCS/LNAI 6803, 2011. ,
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858
A Shallow Embedding of Resolution and Superposition Proofs into the ??-Calculus Modulo, International Workshop on Proof Exchange for Theorem Proving (PxTP), 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01126321
Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps, International Workshop on the Implementation of Logics (IWIL), 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00909688
Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, Logic for Programming Artificial Intelligence and Reasoning (LPAR), pp.10-1007, 2013. ,
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations, Abstract State Machines, Alloy, B, VDM, and Z (ABZ), pp.10-1007, 2014. ,
DOI : 10.1007/978-3-662-43652-3_26
URL : https://hal.archives-ouvertes.fr/hal-00998092
Theorem Proving Modulo, Journal of Automated Reasoning (JAR), vol.31, p.1027357912519, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-01199506
Why3 -Where Programs Meet Provers, European Symposium on Programming (ESOP), 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00789533
A framework for defining logics, Journal of the ACM, vol.40, issue.1, 1993. ,
DOI : 10.1145/138027.138060
A Proposal for Broad Spectrum Proof Certificates, In: Certified Programs and Proofs, vol.4, issue.3, pp.10-1007, 2011. ,
DOI : 10.1007/978-3-540-88387-6_3
URL : https://hal.archives-ouvertes.fr/hal-00772722
H 1 (?Z : Prop. ?H 2 : prf Z. H 2 ) [P : Prop] R Ax P ? ?H 1 : prf P. ?H 2 : prf (¬P) H 2 H 1 [? : type, t : term ?] R = ? t ? ?H 1 : prf (t = ? t) H 1 (?z : (term ? ? Prop) ?H 2 : prf (z t) H 2 ) [? : type, t : term ?, u : term ?] R S ym ? t u ? ?H 1 : prf (t = ? u). ?H 2 : prf (u = ? t) H 2 (?z : (term ? ? Prop). ?H 3 : prf (z u) H 1 (?x : term ?. (z x) ? (z t)) (?H 4 : prf (z t). H 4 ) H 3 ), Prop] R Cut P ? ?H 1 : (prf P ? prf ?). ?H 2 : (prf (¬P) ? prf ?). H 2 H 1 [P : Prop] R ¬¬ P ? ?H 1 : (prf P ? prf ?). ?H 2 : prf (¬¬P). H 2 H 1 [P : Prop, Q : Prop] R ? P Q ? ?H 1 : (prf P ? prf Q ? prf?). ?H 2 : prf (P ? Q). H 2 ? H 1 ,
1 : (t : term ? ? prf (P t) ? prf ?) ?H 2 : prf (? ? P) H 2 ? H 1 [? : type, P : term ? ? Prop, t : term ?] R ? ? P t ? ?H 1 : (prf (P t) ? prf ?). ?H 2 : prf (? ? P) H 1 (H 2 t) [? : type, P : term ? ? Prop, t : term ?] R ¬? ? P t ? ?H 1 : (prf (¬(P t)) ? prf ?), )). H 1 (?H 4 : prf (P t). H 2 (?Z : Prop. ?H 3 : (x : term ? ? prf (P x) ? prf Z). H 3 t H 4 )) ,