Arthur Azevedo de Amorim
where else to find them
what they talk about
where they keep going back
all 4 in the filters
on a stage with
all 12 in the filters
who talks about the same things
- Marco Gaboardi18 talks
- Amal Ahmed25 talks
- Lars Birkedal35 talks
- Leo Stefanesco6 talks
- Edward Lee10 talks
- Joseph Tassarotti20 talks
| title | conference | date |
|---|---|---|
| Cryptis: Cryptographic Reasoning in Separation Logic | POPL 2026 | 2026-01-11 |
Cryptis extends Iris separation logic with a symbolic-cryptography model and gives protocol specs that actually exchange separation-logic resources so proofs… | ||
| Domain Reasoning In TopKAT: Reduction and Completeness | TPSA 2025 | 2025-01-19 |
TopKAT is incomplete over relational models: there exists an inequality true in every relational TopKAT but unprovable from TopKAT axioms, yet adding that… | ||
| Pipelines and Beyond: Graph Types for ADTs with Futures | POPL 2024 | 2024-01-14 |
Extends graph types to let futures live inside recursive ADTs by indexing datatypes with a codata vertex structures that supply unique vertex names, proving… | ||
| Verified Differential Privacy for Finite Computers | CoqPL 2023 | 2023-01-21 |
Coq formalization implements the Geometric Truncated Mechanism using Coq with finprob and rat and proves both an approximate bound (Alpha Prime) and when… | ||
| SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M... | PriSC 2023 | 2023-01-21 |
Extension of CompCert implements CompCert with compartments that enforces interfaces, disables cross-compartment inlining/tailcalls, and updates Coq… | ||
| On Incorrectness Logic and Kleene Algebra with Top and Tests | POPL 2022 | 2022-01-16 |
Kleene Algebra with Tests (KAT) cannot express incorrectness triples because it lacks an explicit codomain operation; adding a single top element yields… | ||
| Deriving Instances with Dependent Types | CoqPL 2020 | 2020-01-25 |
Automates building typeclass instances for Coq inductives: the deriving library generates EQ, Choice, Countable/Fin-like and other instances without plugins… | ||
| nothing matches | ||