Zobrazeno 1 - 6
of 6
pro vyhledávání: '"Coq (logiciel)"'
Autor:
Bartzia, Evmorfia-Iro
Le sujet de ma thèse s’inscrit dans le domaine des preuves formelleset de la vérification des algorithmescryptographiques. L’implémentation des algorithmes cryptographiquesest souvent une tâche assez compliquée, parce qu’ils sont optimisé
Externí odkaz:
http://www.theses.fr/2017SACLX002/document
Autor:
Bartzia, Evmorfia-Iro
Publikováno v:
Cryptography and Security [cs.CR]. Université Paris Saclay (COmUE), 2017. English. ⟨NNT : 2017SACLX002⟩
This thesis is in the domain of formalization of mathematics and ofverification of cryptographic algorithms. The implementation ofcryptographic algorithms is often a complicated task becausecryptographic programs are optimized in order to satisfy bot
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od______2592::259980d2e5a48f76e16bf8a7c79cc44e
https://pastel.archives-ouvertes.fr/tel-01563979/document
https://pastel.archives-ouvertes.fr/tel-01563979/document
Autor:
Wilke, Pierre
Cette thèse présente une extension du compilateur CompCert permettant de fournir des garanties formelles de préservation sémantique à des programmes auxquels CompCert n'en donne pas. CompCert est un compilateur pour le langage C vers différente
Externí odkaz:
http://www.theses.fr/2016REN1S088/document
Autor:
Wilke, Pierre
Publikováno v:
Programming Languages [cs.PL]. Université Rennes 1, 2016. English. ⟨NNT : 2016REN1S088⟩
Programming Languages [cs.PL]. Université de Rennes, 2016. English. ⟨NNT : 2016REN1S088⟩
Programming Languages [cs.PL]. Université de Rennes, 2016. English. ⟨NNT : 2016REN1S088⟩
This thesis presents an extension of the CompCert compiler that aims at providing formal guarantees about the compilation of more programs than CompCert does. The CompCert compiler compiles C code into assembly code for various architectures and prov
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::5501f6a6e7e8b709f977431576b29162
https://tel.archives-ouvertes.fr/tel-01483676
https://tel.archives-ouvertes.fr/tel-01483676
Autor:
Boutillier, Pierre
En ajoutant au lambda-calcul des structures de données algébriques, des types dépendants et un système de modules, on obtient un langage de programmation avec peu de primitives mais une très grande expressivité. L'assistant de preuve Coq s'appu
Autor:
Boutillier, Pierre
Publikováno v:
Langage de programmation [cs.PL]. Université Paris-Diderot-Paris VII, 2014. Français
The dependently typed lambda-calculus with algebraic datastructures is a programming language with very few primitives but a huge expressivity. The Coq proof assistant is built over one variant of this language, the CIC. Its semantics is extremely cl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______212::5701d84deb9ad57dda743d7c02ef172a
https://tel.archives-ouvertes.fr/tel-01054723/file/these_boutillier.pdf
https://tel.archives-ouvertes.fr/tel-01054723/file/these_boutillier.pdf