F. Bobot, S. Conchon, É. Contejean, M. Iguernelala, S. Lescuyer et al., The Alt-Ergo automated theorem prover, 2008.

P. Corbineau, A Declarative Language for the Coq Proof Assistant, Types for Proofs and Programs, International Conference, pp.69-84, 2007.
DOI : 10.1007/978-3-540-68103-8_5

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

G. Gentzen, Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, issue.39, pp.176-210, 1934.
DOI : 10.1007/bf01201353

S. Schulz, System Description: E??0.81, Second International Joint Conference on Automated Reasoning, pp.223-228, 2004.
DOI : 10.1007/978-3-540-25984-8_15

K. Verchinine, A. V. Lyaletski, A. Paskevich, and A. V. Anisimov, On Correctness of Mathematical Texts from a Logical and Practical Point of View, Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium 7th International Conference Proceedings, volume 5144 of Lecture Notes in Computer Science, pp.583-598, 2008.
DOI : 10.1007/978-3-540-85110-3_47

M. M. Wenzel, Isabelle/Isar ? a versatile environment for human-readable formal proof documents, 2002.
DOI : 10.1007/3-540-48256-3_12