-
Semi-automatic verification of cryptographic primitives
CertiCrypt is a framework that enables the machine-checked construction and verification of cryptographic proofs in the Coq proof assistant. CertiCrypt instruments the... -
Design and implementation of a proof verifying kernel for the λΠ-calculus modulo
In recent years, the emergence of feature rich and mature interactive proof assistants has enabled large formalization efforts of high-profile conjectures and results... -
Kleene algebra, Rewriting modulo AC and Circuits in Coq.
This thesis describe three formalisations in Coq. The first chapter is devoted to the implementation of an efficient decision procedure for Kleene algebras : as... -
Formalized algebraic numbers: construction and first-order theory.
This thesis presents a formalization of algebraic numbers and their theory. It brings two new important contributions to the formalization of mathematical results in... -
Interaction between linear algebra and analysis in formal mathematics
In this thesis we present the formalization of three principal results that are the Jordan normal form of a matrix, the Bolzano-Weierstraß theorem, and the... -
Accurate Summation: Towards a Simpler and Formal Proof
Colloque avec actes et comité de lecture. internationale. -
Toward the Integration of Numerical Computations into the OMSCS Framework
Colloque avec actes et comité de lecture. internationale.
