Access control in a core calculus of dependency, Electr. Notes Theor. Comput. Sci, vol.172, pp.5-31, 2007. ,
Deontic Logic in Computer Science, 9th International Conference, Proceedings, vol.5076, pp.96-109, 2008. ,
Secure implementation of channel abstractions, Information and Computation, vol.174, issue.1, pp.37-83, 2002. ,
Infinitesimal: How a dangerous mathematical theory shaped the modern world, 2014. ,
, Accept diversity, 1994.
, Anonymous: The QED manifesto, 12th International Conference on Automated Deduction, pp.238-251, 1994.
Foundational proof-carrying code, 16th Symp. on Logic in Computer Science, pp.247-258, 2001. ,
Proof-carrying authentication, Proceedings of the 6th ACM Conference on Computer and Communications Security, pp.52-62, 1999. ,
A guide to fully homomorphic encryption, Cryptology ePrint Archive, 1192. ,
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
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
Access Control For The Web Via, 2003. ,
IPFS-content addressed, versioned, P2P file system, 2014. ,
Semantic Web road map, W3C Design Issues, 1998. ,
Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
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
A survey of the project AUTOMATH, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp.589-606, 1980. ,
A plea for weaker frameworks, Logical Frameworks, pp.40-67, 1991. ,
A formal model for trust in dynamic networks, SEFM. p. 54, 2003. ,
A review of mathematical knowledge management, Intelligent Computer Mathematics, 16th Symposium, vol.5625, pp.233-246, 2009. ,
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
,
Formal computational unlinkability proofs of RFID protocols, Computer Security Foundations Symposium (CSF), 2017 IEEE 30th, pp.100-114, 2017. ,
A proof-carrying file system, 2010 IEEE Symposium on Security and Privacy, pp.349-364, 2010. ,
A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993. ,
Preface: Twenty years of the QED manifesto, J. Formalized Reasoning, vol.9, issue.1, pp.1-2, 2016. ,
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
Expressing symmetry breaking in DRAT proofs, Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, pp.591-606, 2015. ,
Knowledge and Belief: An Introduction into the logic of the two notions, 1962. ,
QED reloaded: Towards a pluralistic formal library of mathematical knowledge, J. Formalized Reasoning, vol.9, issue.1, pp.201-234, 2016. ,
Mechanizing Proof, 2001. ,
A digital signature based on a conventional encryption function, Advances in Cryptology-CRYPTO '87, vol.293, pp.16-20, 1987. ,
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
,
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
Proof-carrying code, Conference Record of the 24th Symposium on Principles of Programming Languages 97, pp.106-119, 1997. ,
Oracle-based checking of untrusted software, 28th ACM Symp. on Principles of Programming Languages, pp.142-154, 2001. ,
Handbook of Automated Reasoning (in 2 volumes), pp.1063-1147, 2001. ,
How to believe a machine-checked proof, Twenty Five Years of Constructive Type Theory, 1998. ,
A typed natural deduction calculus to reason about secure trust, Twelfth Annual International Conference on Privacy, Security and Trust, pp.379-382, 2014. ,
How to identify, translate and combine logics?, J. of Logic and Computation, vol.27, issue.6, pp.1753-1798, 2017. ,
Nexus Authorization Logic (NAL): Design rationale and applications, ACM Transactions on Information and System Security, vol.14, issue.1, pp.1-8, 2011. ,
,
Hacker-proof coding, Commun. ACM, vol.60, issue.8, pp.12-14, 2017. ,
The certification problem format, Proceedings UITP, pp.61-72, 2014. ,
, Setting the default to reproducible: Reproducibility in computational and experimental mathematics, 2013.
Univalent foundations. Talk given at the Institute for Advanced Study, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00935057
DRAT-trim: Efficient checking and trimming using expressive clausal proofs, Theory and Applications of Satisfiability Testing -SAT 2014, vol.8561, pp.422-429, 2014. ,
The QED manifesto revisited, Studies in Logic, Grammar and Rhetoric, vol.10, issue.23, pp.121-133, 2007. ,
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. ,