Jean-Raymond Abrial (1996):
The B-Book, Assigning Programs to Meanings.
Cambridge University Press,
doi:10.1017/CBO9780511624162.
Hendrik Pieter Barendregt, Wil Dekkers & Richard Statman (2013):
Lambda calculus with types.
Cambridge University Press,
doi:10.1017/CBO9781139032636.
Henk Barendregt & Erik Barendsen (2002):
Autarkic Computations in Formal Proofs.
Journal of Automated Reasoning (JAR) 28,
doi:10.1023/A:1015761529444.
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.
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.
Mathieu Boespflug & Guillaume Burel (2012):
CoqInE: translating the calculus of inductive constructions into the λΠ-calculus modulo.
In: Proof Exchange for Theorem Proving (PxTP).
Mathieu Boespflug, Quentin Carbonneaux & Olivier Hermant (2012):
The λΠ-Calculus Modulo as a Universal Proof Language.
In: Proof Exchange for Theorem Proving (PxTP).
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.
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.
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).
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).
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.
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.
Gilles Dowek, Thérèse Hardin & Claude Kirchner (2003):
Theorem Proving Modulo.
Journal of Automated Reasoning (JAR) 31,
doi:10.1023/A:1027357912519.
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.
Thérèse Hardin, François Pessaux, Pierre Weis & Damien Doligez (2009):
FoCaLiZe reference manual.
Robert Harper, Furio Honsell & Gordon Plotkin (1993):
A Framework for Defining Logics.
Journal of the ACM 40,
doi:10.1145/138027.138060.
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.
eptcs@eptcs.org