Bas Spitters
where else to find them
what they talk about
all 6 in the filters
where they keep going back
- CPP3 editions2023–2025
on a stage with
all 13 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq | CPP 2025 | 2025-01-20 |
A verified backend implemented and proven in Coq generates WebAssembly modules from CertiCoq’s Lambda ANF, mechanised against WasmCert-Coq and offering a… | ||
| CertiCoq-Wasm: Verified compilation from Coq to WebAssembly | CoqPL 2024 | 2024-01-20 |
A verified compiler from Gallina (Coq) to WebAssembly is implemented and mechanised against the WasmCert-Coq formalisation, reusing the CertiCoq pipeline and… | ||
| Specifying Smart Contract with Hax and ConCert | CoqPL 2024 | 2024-01-20 |
A reproducible toolchain embeds Rust-style smart contracts into Hax, rewrites mutable state into message-passing state, annotates properties, and translates… | ||
| A formal security analysis of Blockchain voting | CoqPL 2024 | 2024-01-20 |
Formal Coq development models the Open Vote Network and proves provably functionally correct behavior plus cryptographically secure properties: self‑tallying… | ||
| The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography | CPP 2024 | 2024-01-15 |
Coq is used to connect Hacspec, Jasmin and SSProve into an automated pipeline that produces: a functional Hacspec spec, an imperative SSProve spec, and… | ||
| Formalising Decentralised Exchanges in Coq | CPP 2023 | 2023-01-16 |
Claims a first formalisation in Coq of a decentralized exchange implementation (Dexter2) capturing cross-contract interactions, proves functional correctness… | ||
| Code Extraction from Coq to ML-like languages | ML 2021 | 2021-08-26 |
Pipeline implemented wholly in Coq uses MetaCoq's verified erasure to produce a typed intermediate lambda-box-t representation, runs a certifying preprocessing… | ||
| nothing matches | ||