@book(B-Book,
 author       = {Jean-Raymond Abrial},
 year         = {1996},
 title        = {The {\textsf{B}-Book{}}, Assigning Programs to Meanings},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511624162},
)
@book(barendregt2013lambda,
 author       = {Hendrik Pieter Barendregt and Wil Dekkers and Richard Statman},
 year         = {2013},
 title        = {Lambda calculus with types},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139032636},
)
@article(BB02,
 author       = {Henk Barendregt and Erik Barendsen},
 year         = {2002},
 title        = {{Autarkic Computations in Formal Proofs}},
 journal      = {Journal of Automated Reasoning (JAR)},
 volume       = {28},
 doi          = {10.1023/A:1015761529444},
)
@inproceedings(barnett2006boogie,
 author       = {Mike Barnett and Bor-Yuh Evan Chang and Robert DeLine and Bart Jacobs and K Rustan M Leino},
 year         = {2006},
 title        = {Boogie: A modular reusable verifier for object-oriented programs},
 booktitle    = {Formal Methods for Components and Objects},
 organization = {Springer},
 doi          = {10.1007/11804192\_17},
)
@inproceedings(TFF1,
 author       = {Jasmin Christian Blanchette and Andrei Paskevich},
 year         = {2013},
 title        = {{{TFF1}: The {TPTP} Typed First-Order Form with Rank-1 Polymorphism}},
 booktitle    = {Conference on Automated Deduction (CADE)},
 series       = {LNCS},
 volume       = {7898},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-38574-2\_29},
)
@inproceedings(boespflug2012coqine,
 author       = {Mathieu Boespflug and Guillaume Burel},
 year         = {2012},
 title        = {{CoqInE}: translating the calculus of inductive constructions into the {$\lambda\Pi $}-calculus modulo},
 booktitle    = {Proof Exchange for Theorem Proving (PxTP)},
)
@inproceedings(BA12,
 author       = {Mathieu Boespflug and Quentin Carbonneaux and Olivier Hermant},
 year         = {2012},
 title        = {{The {$\lambda\Pi $}-Calculus Modulo as a Universal Proof Language}},
 booktitle    = {Proof Exchange for Theorem Proving (PxTP)},
)
@inproceedings(Zenon,
 author       = {Richard Bonichon and David Delahaye and Damien Doligez},
 year         = {2007},
 title        = {{{\textsf{Zenon}{}}: An Extensible Automated Theorem Prover Producing Checkable Proofs}},
 booktitle    = {Logic for Programming Artificial Intelligence and Reasoning (LPAR)},
 series       = {LNCS/LNAI},
 volume       = {4790},
 publisher    = {Springer},
 doi          = {10.1007/978-3-540-75560-9\_13},
)
@inproceedings(GB11b,
 author       = {Guillaume Burel},
 year         = {2011},
 title        = {{Experimenting with Deduction Modulo}},
 booktitle    = {Conference on Automated Deduction (CADE)},
 series       = {LNCS/LNAI},
 volume       = {6803},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-22438-6\_14},
)
@inproceedings(burel2013shallow,
 author       = {Guillaume Burel},
 year         = {2013},
 title        = {A Shallow Embedding of Resolution and Superposition Proofs into the {$\lambda\Pi $}-Calculus Modulo},
 booktitle    = {International Workshop on Proof Exchange for Theorem Proving (PxTP)},
)
@misc(focalide,
 author       = {Rapha\"{e}l Cauderlier},
 title        = {Focalide},
 howpublished = {\url{https://www.rocq.inria.fr/deducteam/Focalide}},
)
@inproceedings(Zenon-Modulo2,
 author       = {David Delahaye and Damien Doligez and Fr\'{e}d\'{e}ric Gilbert and Pierre Halmagrand and Olivier Hermant},
 year         = {2013},
 title        = {{Proof Certification in {\textsf{Zenon~Modulo}}: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps}},
 booktitle    = {International Workshop on the Implementation of Logics (IWIL)},
)
@inproceedings(Zenon-Modulo,
 author       = {David Delahaye and Damien Doligez and Fr\'{e}d\'{e}ric Gilbert and Pierre Halmagrand and Olivier Hermant},
 year         = {2013},
 title        = {{{\textsf{Zenon~Modulo}{}}: When Achilles Outruns the Tortoise using Deduction Modulo}},
 booktitle    = {Logic for Programming Artificial Intelligence and Reasoning (LPAR)},
 series       = {LNCS/ARCoSS},
 volume       = {8312},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-45221-5\_20},
)
@inproceedings(BWare,
 author       = {David Delahaye and Catherine Dubois and Claude March\'{e} and David Mentr\'{e}},
 year         = {2014},
 title        = {{The {\textsf{BWare}{}} Project: Building a Proof Platform for the Automated Verification of {\textsf{B}{}} Proof Obligations}},
 booktitle    = {Abstract State Machines, \textsf{Alloy}{}, \textsf{B}{}, \textsf{VDM}{}, and \textsf{Z}{} (ABZ)},
 series       = {LNCS},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-43652-3\_26},
)
@article(DA03,
 author       = {Gilles Dowek and Th\'{e}r\`{e}se Hardin and Claude Kirchner},
 year         = {2003},
 title        = {{Theorem Proving Modulo}},
 journal      = {Journal of Automated Reasoning (JAR)},
 volume       = {31},
 doi          = {10.1023/A:1027357912519},
)
@inproceedings(FP13,
 author       = {Jean{-}Christophe Filli{\^{a}}tre and Andrei Paskevich},
 year         = {2013},
 title        = {Why3 - Where Programs Meet Provers},
 booktitle    = {European Symposium on Programming (ESOP)},
 doi          = {10.1007/978-3-642-37036-6\_8},
)
@manual(focalize,
 author       = {Th\'{e}r\`{e}se Hardin and Fran\c{c}ois Pessaux and Pierre Weis and Damien Doligez},
 year         = {2009},
 title        = {{FoCaLiZe} reference manual},
)
@article(Harper1993,
 author       = {Robert Harper and Furio Honsell and Gordon Plotkin},
 year         = {1993},
 title        = {A Framework for Defining Logics},
 journal      = {Journal of the ACM},
 volume       = {40},
 doi          = {10.1145/138027.138060},
)
@incollection(miller2011proposal,
 author       = {Dale Miller},
 year         = {2011},
 title        = {A proposal for broad spectrum proof certificates},
 booktitle    = {Certified Programs and Proofs (CPP)},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-25379-9\_6},
)