1. Jean-Raymond Abrial (1996): The B-Book, Assigning Programs to Meanings. Cambridge University Press, doi:10.1017/CBO9780511624162.
  2. Hendrik Pieter Barendregt, Wil Dekkers & Richard Statman (2013): Lambda calculus with types. Cambridge University Press, doi:10.1017/CBO9781139032636.
  3. Henk Barendregt & Erik Barendsen (2002): Autarkic Computations in Formal Proofs. Journal of Automated Reasoning (JAR) 28, doi:10.1023/A:1015761529444.
  4. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs & K Rustan M Leino (2006): Boogie: A modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects. Springer, doi:10.1007/11804192_17.
  5. Jasmin Christian Blanchette & Andrei Paskevich (2013): TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. In: Conference on Automated Deduction (CADE), LNCS 7898. Springer, doi:10.1007/978-3-642-38574-2_29.
  6. Mathieu Boespflug & Guillaume Burel (2012): CoqInE: translating the calculus of inductive constructions into the λΠ-calculus modulo. In: Proof Exchange for Theorem Proving (PxTP).
  7. Mathieu Boespflug, Quentin Carbonneaux & Olivier Hermant (2012): The λΠ-Calculus Modulo as a Universal Proof Language. In: Proof Exchange for Theorem Proving (PxTP).
  8. Richard Bonichon, David Delahaye & Damien Doligez (2007): Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs. In: Logic for Programming Artificial Intelligence and Reasoning (LPAR), LNCS/LNAI 4790. Springer, doi:10.1007/978-3-540-75560-9_13.
  9. Guillaume Burel (2011): Experimenting with Deduction Modulo. In: Conference on Automated Deduction (CADE), LNCS/LNAI 6803. Springer, doi:10.1007/978-3-642-22438-6_14.
  10. Guillaume Burel (2013): A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. In: International Workshop on Proof Exchange for Theorem Proving (PxTP).
  11. Raphaël Cauderlier: Focalide.
  12. David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand & Olivier Hermant (2013): Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. In: International Workshop on the Implementation of Logics (IWIL).
  13. David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand & Olivier Hermant (2013): Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. In: Logic for Programming Artificial Intelligence and Reasoning (LPAR), LNCS/ARCoSS 8312. Springer, doi:10.1007/978-3-642-45221-5_20.
  14. David Delahaye, Catherine Dubois, Claude Marché & David Mentré (2014): The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. In: Abstract State Machines, Alloy, B, VDM, and Z (ABZ), LNCS. Springer, doi:10.1007/978-3-662-43652-3_26.
  15. Gilles Dowek, Thérèse Hardin & Claude Kirchner (2003): Theorem Proving Modulo. Journal of Automated Reasoning (JAR) 31, doi:10.1023/A:1027357912519.
  16. Jean-Christophe Filliâtre & Andrei Paskevich (2013): Why3 - Where Programs Meet Provers. In: European Symposium on Programming (ESOP), doi:10.1007/978-3-642-37036-6_8.
  17. Thérèse Hardin, François Pessaux, Pierre Weis & Damien Doligez (2009): FoCaLiZe reference manual.
  18. Robert Harper, Furio Honsell & Gordon Plotkin (1993): A Framework for Defining Logics. Journal of the ACM 40, doi:10.1145/138027.138060.
  19. Dale Miller (2011): A proposal for broad spectrum proof certificates. In: Certified Programs and Proofs (CPP). Springer, doi:10.1007/978-3-642-25379-9_6.

Comments and questions to:
For website issues: