Bertot, Yves.
Bertot, Yves, 1964-....
Yves Bertot francouzský matematik, informatik
VIAF ID: 8238368 ( Personal )
Permalink: http://viaf.org/viaf/8238368
Preferred Forms
-
-
- 100 1 _ ‡a Bertot, Yves
-
-
-
-
- 100 1 _ ‡a Bertot, Yves
- 100 1 _ ‡a Bertot, Yves
-
- 100 1 _ ‡a Bertot, Yves, ‡d 1964-....
-
- 100 0 _ ‡a Yves Bertot ‡c francouzský matematik, informatik
4xx's: Alternate Name Forms (2)
Works
Title | Sources |
---|---|
ANALYSING PROGRAMS ANNOTATED BY ASSERTIONS. | |
Une automatisation du calcul des residus en semantique naturelle | |
An automatization of residual computations in natural semantics. | |
Bibliothèque certifiée en Coq pour la provenance des données | |
Certification of an Instruction Set Simulator | |
Changing data representation in the calculus of constructions. | |
Communicating automata and quasi-synchronous communications. | |
Contributions to the Formal Verification of Arithmetic Algorithms. | |
A Coq certified library for data provenance. | |
Coq formalization of digital filter algorithms computed using finite precision arithmetic. | |
Des environnements de programmation aux environnements de preuve | |
Étude formelle d'algorithmes efficaces en algèbre linéaire | |
Explication textuelle de preuves pour le calcul des constructions inductives : thèse ... | |
Fonctions récursives générales dans le calcul des constructions | |
Formal description of geometric properties. | |
Formal proof in network calculus. | |
Formal Security Proofs of Cryptographic : A necessity achieved using EasyCrypt. | |
Formal study of efficient algorithms in linear algebra. | |
Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie | |
Formalisations d'analyses d'erreurs en analyse numérique et en arithmétique à virgule flottante | |
Formalisations en Coq pour la décision de problèmes en géométrie algébrique réelle | |
Formalizations of error analysis in numerical analysis and floating-point arithmetic. | |
Formally computer-verified protections against timing-based side-channel attacks. | |
From semantics to computer science : essays in honour of Gilles Kahn | |
Génération de codes et d'annotations prouvables d'algorithmes de points intérieurs à destination de systèmes embarqués critiques | |
Implementation of an interpreter for a parallel language in Centaur | |
Interaction entre algèbre linéaire et analyse en formalisation des mathématiques | |
Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions | |
Interfaces utilisateur pour les prouveurs de théorèmes : 1-2 septembre 1997 : actes = Proceedings user interfaces for theorem provers : september 1-2, 1997 : proceedings : Sophia Antipolis, France | |
Mechanized support for the formal specification, verification and deployment of component-based applications. | |
Occurrences in debugger specifications = Utilisation d'occurrences dans la spécification d'outils de mise au point | |
Outils pour la formalisation en analyse classique : une étude de cas en théorie du contrôle | |
Preuve formelle en calcul réseau | |
Preuves formelles de la sécurité de standards : Un objectif nécessaire, possible grâce à EasyCrypt | |
Protections vérifiées formellement par ordinateur contre les attaques par canaux auxiliaires basées sur le temps | |
Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis. | |
Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée | |
Theorem proving in higher order logics : 12th international conference, TPHOLs '99, Nice, France, September 14-17, 1999 : proceedings | |
Une théorie des types avec insignifiance des preuves définitionnelle. | |
TPHOLs'99 | |
Type theoretic semantics for programming languages | |
A type theory with definitional proof-irrelevance | |
UITP'97 : proceedings = actes | |
Vérification formelle pour les méthodes numériques | |
Vérification mécanisée de la correction et complexité asymptotique de programmes. | |
Vérification semi-automatique de primitives cryptographiques | |
Verified computing in homological algebra : a journey exploring the power and limits of dependent type theory |