Q. Rules and . Subst, 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?)

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

A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Dedukti: a Logical Framework based on the ??-Calculus Modulo Theory, 2016.

A. Assaf and G. Burel, Translating HOL to Dedukti. arXiv preprint, 2015.
DOI : 10.4204/eptcs.186.8
URL : https://hal.archives-ouvertes.fr/hal-01097412

R. Bagnara, On the Toyota UA Case and the Redefinition of Product Liability for Embedded Software, 2014.

H. Pieter-barendregt, W. Dekkers, and R. Statman, Lambda Calculus with Types, 2013.
DOI : 10.1017/CBO9781139032636

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

P. Behm, P. Benoit, A. Faivre, and J. Meynadier, M??t??or: A Successful Application of B in a Large Project, International Symposium on Formal Methods, pp.369-387, 1999.
DOI : 10.1007/3-540-48119-2_22

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development: Coq'Art: the Calculus of Inductive Constructions, 2013.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

W. Evert and . Beth, Semantic Entailment and Formal Derivability Koninklijke Nederlandse Akademie van Wentenschappen, Proceedings of the Section of Sciences, pp.309-342276, 1955.

J. Christian-blanchette and A. Paskevich, TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism, Conference on Automated Deduction (CADE), 2013.

J. Christian-blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding Monomorphic and Polymorphic Types, pp.493-507978

J. Christian-blanchette, S. Böhme, M. Fleury, S. J. Smolka, and A. Steckermeier, Semi-intelligible Isar Proofs from Machine-Generated Proofs, Journal of Automated Reasoning

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd Your Herd of Provers, International Workshop on Intermediate Verification Languages (Boogie), 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

F. Bobot, S. Conchon, and E. Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo Automated Theorem Prover, 2008.

M. Boespflug and G. Burel, CoqInE: Translating the Calculus of Inductive Constructions into the ??-calculus modulo, Proof Exchange for Theorem Proving (PxTP), 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126128

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs Principles of Superdeduction, Logic for Programming Artificial Intelligence and Reasoning (LPAR) 22nd Annual IEEE Symposium on Logic in Computer Science, pp.41-50, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.2082

G. Burel, Experimenting with Deduction Modulo, Conference on Automated Deduction (CADE), 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

G. Bury and D. Delahaye, Integrating Simplex with Tableaux, Automated Reasoning with Analytic Tableaux and Related Methods, 24th International Conference. Proceedings, pp.86-101, 2015.
DOI : 10.1007/978-3-319-24312-2_7
URL : https://hal.archives-ouvertes.fr/hal-01215490

G. Bury, R. Cauderlier, and P. Halmagrand, Implementing Polymorphism in Zenon URL https, 11th International Workshop on the Implementation of Logics (IWIL), 2015.

G. Bury, D. Delahaye, D. Doligez, P. Halmagrand, and O. Hermant, Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo URL https, LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2015.

R. Cauderlier, Object-Oriented Mechanisms for Interoperability between Proof Systems. Theses, Conservatoire national des arts et metiers -CNAM, 2016. URL https://who. rocq.inria.fr/Raphael
URL : https://hal.archives-ouvertes.fr/tel-01415945

R. Cauderlier and P. Halmagrand, Checking Zenon Modulo Proofs in Dedukti URL https, Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), 2015.
DOI : 10.4204/eptcs.186.7
URL : http://doi.org/10.4204/eptcs.186.7

M. Chafkin, Uber's First Self-Driving Fleet Arrives in Pittsburgh This Month http://www.bloomberg.com/news/features/2016-08-18/ uber-s-first-self-driving-fleet-arrives-in-pittsburgh-this-month-is06r7on, 2016.

S. Cruanes, Extending Superposition with Integer Arithmetic, Structural Induction , and Beyond. Theses, École polytechnique, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01223502

D. Marcello, . Agostino, M. Dov, R. Gabbay, J. Hähnle et al., Handbook of Tableau Methods, 2013.

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, 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, C. Dubois, C. Marché, and D. 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), 2014.
DOI : 10.1007/978-3-662-43652-3_26
URL : https://hal.archives-ouvertes.fr/hal-00998092

G. Dowek and A. Miquel, Cut elimination for Zermelo set theory. Archive for Mathematical Logic, 2007.

G. Dowek, T. Hardin, and C. Kirchner, Theorem Proving Modulo, Journal of Automated Reasoning, p.31, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00077199

C. Favre, Fly-by-wire for commercial aircraft: the Airbus experience, International Journal of Control, vol.59, issue.1, pp.139-157, 1994.
DOI : 10.1080/00207179408923072

G. Gentzen, Untersuchungen über das logische Schließen. I. Mathematische zeitschrift, pp.176-210, 1935.
DOI : 10.1007/bf01201353

M. Giese and W. Ahrendt, Hilbert???s ???-Terms in Automated Theorem Proving, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp.171-185, 1999.
DOI : 10.1007/3-540-48754-9_17

R. Goré, Tableau Methods for Modal and Temporal Logics, Handbook of tableau methods, pp.297-396, 1999.
DOI : 10.1007/978-94-017-1754-0_6

P. Halmagrand, Soundly Proving B Method Formul?? Using Typed Sequent Calculus, 13th International Colloquium on Theoretical Aspects of Computing (ICTAC), 2016.
DOI : 10.1007/978-3-642-30885-7_17
URL : https://hal.archives-ouvertes.fr/hal-01342849/document

T. Hardin, F. Pessaux, P. Weis, and D. Doligez, FoCaLiZe-Reference Manual, p.50, 2009.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, 1993.
DOI : 10.1145/138027.138060
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.5854

J. Hintikka, Form and Content in Quantification Theory, Acta Philosophica Fennica, vol.8, issue.7, p.55, 1955.

M. Jacquel, Proof Automation for Atelier B Rules Verification. Theses, Conservatoire national des arts et metiers -CNAM URL https, 2013.
URL : https://hal.archives-ouvertes.fr/tel-00840484

M. Jacquel, K. Berkani, D. Delahaye, and C. Dubois, Tableaux Modulo Theories Using Superdeduction, International Joint Conference on Automated Reasoning, pp.332-338, 2012.
DOI : 10.1007/978-3-642-31365-3_26
URL : https://hal.archives-ouvertes.fr/hal-01099338

F. Kirchner, A Finite First-Order Theory of Classes, Types for Proofs and Programs, pp.188-202, 2006.
DOI : 10.1007/978-3-540-74464-1_13

P. Koopman, A Case Study of Toyota Unintended Acceleration and Software Safety, 2014.

K. Korovin, iProver ??? An Instantiation-Based Theorem Prover for First-Order Logic (System Description), International Joint Conference on Automated Reasoning, pp.292-298, 2008.
DOI : 10.1007/978-3-540-71070-7_24

R. Lardennois and . Val, VAL automated guided transit characteristics and evolutions, Journal of Advanced Transportation, vol.27, issue.1, pp.103-120, 1993.
DOI : 10.1002/atr.5670270109

D. Mentré, C. Marché, J. Filliâtre, and M. Asuka, Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, Abstract State Machines, Alloy, B, VDM, and Z (ABZ), 2012.
DOI : 10.1007/978-3-642-30885-7_17

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving. Handbook of automated reasoning, pp.371-443, 2001.
DOI : 10.1016/b978-044450813-3/50009-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.6344

D. Pham, Reconstruction de Preuves au Format TSTP pour Dedukti, 2016.

A. Sage and P. Lienert, Ford Plans Self-Driving Car for Ride Share Fleets in 2021, 2016.

R. Saillard, Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. Theses, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01299180

S. Schulz, System Description: E??1.8
DOI : 10.1007/978-3-642-45221-5_49

M. Raymond and . Smullyan, First-Order Logic, Courier Corporation, 1995.

C. Strachey, Fundamental Concepts in Programming Languages. Higher-order and symbolic computation, pp.11-49, 2000.

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

G. Sutcliffe, The CADE ATP System Competition -CASC. AI Magazine, pp.99-101, 2016.
DOI : 10.1007/978-3-540-25984-8_36
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.119.2296

D. Wand, Polymorphic+Typeclass Superposition, Practical Aspects of Automated Reasoning URL, p.15, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01098078

C. Weidenbach and . Spass, Combining Superposition, Sorts and Splitting. Handbook of automated reasoning, pp.1965-2013, 1999.
DOI : 10.1016/b978-044450813-3/50029-1
URL : http://hdl.handle.net/11858/00-001M-0000-000F-31F3-8