J. Abrial, The B-Book, Assigning Programs to Meanings, pp.10-1017, 1996.

H. Pieter-barendregt and R. Statman, Lambda calculus with types, pp.10-1017, 2013.
DOI : 10.1017/CBO9781139032636

H. Barendregt and &. Barendsen, Autarkic Computations in Formal Proofs, Journal of Automated Reasoning (JAR), vol.28, p.1015761529444, 2002.

M. Barnett, R. Bor-yuh-evan-chang, B. Deline, &. Jacobs, M. Rustan et al., Boogie: A modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects, pp.10-1007, 2006.

J. Paskevich, 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

M. Boespflug and &. Burel, CoqInE: translating the calculus of inductive constructions into the ??-calculus modulo, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126128

M. Boespflug, Q. Carbonneaux, and &. Olivier-hermant, The ??-Calculus Modulo as a Universal Proof Language, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

R. Bonichon, D. , and D. Doligez, 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

G. Burel, 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

G. Burel, 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

D. Delahaye, D. Doligez, and F. Gilbert, 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

D. Delahaye, D. Doligez, and F. Gilbert, 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

D. Delahaye, C. Dubois, C. Marché, and &. David-mentré, 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

G. Dowek, T. Hardin, and C. Kirchner, Theorem Proving Modulo, Journal of Automated Reasoning (JAR), vol.31, p.1027357912519, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01199506

J. Paskevich, Why3 -Where Programs Meet Provers, European Symposium on Programming (ESOP), 2013.
URL : https://hal.archives-ouvertes.fr/hal-00789533

R. Harper, F. Honsell, and &. Gordon-plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, 1993.
DOI : 10.1145/138027.138060

D. Miller, 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. Llproof-inference-rules-[-]-r-?-?-?h-prf and . ?h, 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

?. Prop and ]. ?h, 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 ))