M. Abadi, Access control in a core calculus of dependency, Electr. Notes Theor. Comput. Sci, vol.172, pp.5-31, 2007.

M. Abadi, Deontic Logic in Computer Science, 9th International Conference, Proceedings, vol.5076, pp.96-109, 2008.

M. Abadi, C. Fournet, and G. Gonthier, Secure implementation of channel abstractions, Information and Computation, vol.174, issue.1, pp.37-83, 2002.

A. Alexander, Infinitesimal: How a dangerous mathematical theory shaped the modern world, 2014.

P. B. Andrews, Accept diversity, 1994.

, Anonymous: The QED manifesto, 12th International Conference on Automated Deduction, pp.238-251, 1994.

A. W. Appel, Foundational proof-carrying code, 16th Symp. on Logic in Computer Science, pp.247-258, 2001.

A. W. Appel and E. W. Felten, Proof-carrying authentication, Proceedings of the 6th ACM Conference on Computer and Communications Security, pp.52-62, 1999.

F. Armknecht, C. Boyd, C. Carr, K. Gjøsteen, A. Jäschke et al., A guide to fully homomorphic encryption, Cryptology ePrint Archive, 1192.

A. Assaf and G. Burel, Translating HOL to Dedukti, Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, vol.186, pp.74-88, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01097412

A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Expressing theories in the ??calculus modulo theory and in the Dedukti system, TYPES: Types for Proofs and Programs, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01441751

L. Bauer, Access Control For The Web Via, 2003.

J. Benet, IPFS-content addressed, versioned, P2P file system, 2014.

T. Berners-lee, Semantic Web road map, W3C Design Issues, 1998.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

R. Blanco, Z. Chihani, and D. Miller, Translating between implicit and explicit versions of proof, CADE 26 -International Conference on Automated Deduction, vol.10395, pp.255-273, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01645016

N. G. De-bruijn, A survey of the project AUTOMATH, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp.589-606, 1980.

N. G. De-bruijn, A plea for weaker frameworks, Logical Frameworks, pp.40-67, 1991.

M. Carbone, M. Nielsen, and V. Sassone, A formal model for trust in dynamic networks, SEFM. p. 54, 2003.

J. Carette and W. M. Farmer, A review of mathematical knowledge management, Intelligent Computer Mathematics, 16th Symposium, vol.5625, pp.233-246, 2009.

Z. Chihani, D. Miller, and F. Renaud, A semantic framework for proof evidence, J. of Automated Reasoning, vol.59, issue.3, pp.287-330, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01390912

,

H. Comon and A. Koutsos, Formal computational unlinkability proofs of RFID protocols, Computer Security Foundations Symposium (CSF), 2017 IEEE 30th, pp.100-114, 2017.

D. Garg and F. Pfenning, A proof-carrying file system, 2010 IEEE Symposium on Security and Privacy, pp.349-364, 2010.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.

J. Harrison, J. Urban, and F. Wiedijk, Preface: Twenty years of the QED manifesto, J. Formalized Reasoning, vol.9, issue.1, pp.1-2, 2016.

Q. Heath and D. Miller, A proof theory for model checking, J. of Automated Reasoning, vol.63, issue.4, pp.857-885, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01814006

M. Heule, W. A. Jr, and N. Wetzler, Expressing symmetry breaking in DRAT proofs, Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, pp.591-606, 2015.

J. Hintikka, Knowledge and Belief: An Introduction into the logic of the two notions, 1962.

M. Kohlhase and F. Rabe, QED reloaded: Towards a pluralistic formal library of mathematical knowledge, J. Formalized Reasoning, vol.9, issue.1, pp.201-234, 2016.

D. Mackenzie, Mechanizing Proof, 2001.

R. C. Merkle, A digital signature based on a conventional encryption function, Advances in Cryptology-CRYPTO '87, vol.293, pp.16-20, 1987.

D. Miller, A proposal for broad spectrum proof certificates, CPP: First International Conference on Certified Programs and Proofs, vol.7086, pp.54-69, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00772722

,

D. Miller, Proof checking and logic programming, Formal Aspects of Computing, vol.29, issue.3, pp.383-399, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01390901

G. C. Necula, Proof-carrying code, Conference Record of the 24th Symposium on Principles of Programming Languages 97, pp.106-119, 1997.

G. C. Necula and S. P. Rahul, Oracle-based checking of untrusted software, 28th ACM Symp. on Principles of Programming Languages, pp.142-154, 2001.

F. Pfenning, Handbook of Automated Reasoning (in 2 volumes), pp.1063-1147, 2001.

R. Pollack, How to believe a machine-checked proof, Twenty Five Years of Constructive Type Theory, 1998.

G. Primiero, F. Raimondi, A. Miri, U. Hengartner, N. F. Huang et al., A typed natural deduction calculus to reason about secure trust, Twelfth Annual International Conference on Privacy, Security and Trust, pp.379-382, 2014.

F. Rabe, How to identify, translate and combine logics?, J. of Logic and Computation, vol.27, issue.6, pp.1753-1798, 2017.

F. B. Schneider, K. Walsh, and E. G. Sirer, Nexus Authorization Logic (NAL): Design rationale and applications, ACM Transactions on Information and System Security, vol.14, issue.1, pp.1-8, 2011.

,

E. Shein, Hacker-proof coding, Commun. ACM, vol.60, issue.8, pp.12-14, 2017.

C. Sternagel and R. Thiemann, The certification problem format, Proceedings UITP, pp.61-72, 2014.

V. Stodden, D. H. Bailey, J. Borwein, R. J. Leveque, W. Rider et al., Setting the default to reproducible: Reproducibility in computational and experimental mathematics, 2013.

V. Voevodsky, Univalent foundations. Talk given at the Institute for Advanced Study, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00935057

N. Wetzler, M. J. Heule, and J. W. Hunt, DRAT-trim: Efficient checking and trimming using expressive clausal proofs, Theory and Applications of Satisfiability Testing -SAT 2014, vol.8561, pp.422-429, 2014.

F. Wiedijk, The QED manifesto revisited, Studies in Logic, Grammar and Rhetoric, vol.10, issue.23, pp.121-133, 2007.

D. Wu, A. W. Appel, and A. Stump, Foundational proof checkers with small witnesses, PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pp.264-274, 2003.