53 citations
- Institut national de recherche en sciences et technologies du numériqueFR6 papers
- Centre Inria de SaclayFR3 papers
- Microsoft (United States)US3 papers
- Equipes Traitement de l'Information et SystèmesFR2 papers
- PROSECCO: Programming securely with cryptographyFR2 papers
- Alexandru Ioan Cuza UniversityRO1 paper
- Centre Inria de l'Université de LorraineFR1 paper
- Centre National de la Recherche ScientifiqueFR1 paper
- COSMIQ: Cryptologie symétrique, cryptologie fondée sur les codes et information quantiqueFR1 paper
- CY Cergy Paris UniversitéFR1 paper
- École Normale Supérieure de LyonFR1 paper
- École Normale Supérieure - PSLFR1 paper
Showing cs.PLShow all
3 papers · 1 filter
cs.PL2023★ 5 cited
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu +4
We introduce SCIO*, a formally secure compilation framework for statically verified partial programs performing input-output (IO). The source language is an F* subset in which a ve…
cs.PL2022★ 46 cited
Aeneas: Rust Verification by Functional Translation
Son Ho, Jonathan Protzenko
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust's rich region-based type system to eliminate memor…
cs.PL2021★ 53 cited
Catala: A Programming Language for the Law
Denis Merigoux, Nicolas Chataing, Jonathan Protzenko
Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout…