Danil Annenkov
where else to find them
what they talk about
where they keep going back
- CPP2 editions2020–2023
on a stage with
- Bas Spitters2×
- Eske Hoy Nielsenonce
- Mikkel Miloonce
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| 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… | ||
| ConCert: A Smart Contract Certification Framework in Coq | CPP 2020 | 2020-01-20 |
Framework converts ACORN smart contracts into Coq functions via MetaCoq, proves computational soundness of the translation, and embeds the resulting functions… | ||
| nothing matches | ||