| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Fri, 02 Dec 2022 09:58:21 GMT
access-control-allow-origin: *
etag: W/"6389cc3d-b94"
expires: Mon, 29 Dec 2025 16:34:25 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 669D:272D88:9201E4:A3AB43:6952AB38
accept-ranges: bytes
age: 0
date: Mon, 29 Dec 2025 16:24:25 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210090-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767025465.117938,VS0,VE205
vary: Accept-Encoding
x-fastly-request-id: d7264f65564721f7c265ed67cf0b8775cdc35419
content-length: 1235
Pierre-Yves Strub
Email: pierre-yves [at] strub.nu
Software
- EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs.
- Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant.
- Coq Modulo Theory is an extension of the Coq proof assistant embedding, in its computational mechanism, validity entailment for user-defined first-order equational theories.
- Some of my developments can be found on my github profile.
Download
- The last version of EasyCrypt can be found on the EasyCrypt website.
- The last version of CoqMT is 8.3pl3. You can browse the sources repository.
Publications
The following list of publications has been extracted from my DBLP page.