Dominique Devriese
where else to find them
linkedin:dominique-devriese-9905757
what they talk about
where they keep going back
all 7 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Thomas Van Strydonck5 talks
- Kenji Maillard11 talks
- Armaël Guéneau7 talks
- Nicolas Tabareau14 talks
- Amin Timany16 talks
- Lars Birkedal35 talks
| title | conference | date |
|---|---|---|
| Cerisier: A Program Logic for Attestation in a Capability Machine | PLDI 2026 | 2026-06-15 |
Cerisier presents a program logic that formalizes CHERI-TrEE support for enclaves on a capability machine and claims modular, end-to-end proofs for systems… | ||
| PC Chair Report | ICFP 2025 | 2025-10-12 |
Program committee reports 110 submissions and 36 acceptances (≈33%), with nine JFP journal‑first papers included. A two‑round process enforces mandatory… | ||
| Award Ceremony | ICFP 2025 | 2025-10-12 |
Selection process reports that 10 papers nominated are reviewed by a committee of six senior non‑conflicted members who meet twice and pick four distinguished… | ||
| BiSikkel: A Multimode Logical Framework in Agda | POPL 2025 | 2025-01-19 |
Library implements a multimode logical framework (MULF) on top of the existing Sikkel Agda stack, giving a syntactic MST layer, presheaf semantics and a… | ||
| Secure Calling Conventions for CHERI Capability Machines in Practice (Work in P... | PriSC 2024 | 2024-01-20 |
Proposes a concrete design that reconciles theoretical secure calling conventions with real CHERI-RISC-V constraints by introducing a reserve stack to avoid… | ||
| Proving capability safety in the presence of indirect sentries | POCL 2024 | 2024-01-16 |
Extends a CHERI-style miniature machine (SeRiES) with indirect sentries, adapts an Iris-like program logic plus a new logical relation, and produces… | ||
| Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Pr... | POCL 2024 | 2024-01-16 |
Implements CHERI calling conventions in LLVM and shows a concrete fix for CHERI’s lossy capability compression: split the stack into an active/reserve stack so… | ||
| Internal and Observational Parametricity for Cubical Agda | POPL 2024 | 2024-01-14 |
An implementation called Agda --bridges adds internal parametricity to cubical Agda, successfully type checks the cubical library and mechanizes key results… | ||
| pi_RA: A pi-calculus for verifying protocols that use remote attestation | PriSC 2023 | 2023-01-21 |
pi_RA is an applied pi-calculus variant that treats remote attestation as a first‑class cryptographic primitive and compiles an actor-style source language… | ||
| Plausible sealing for gradual parametricity | OOPSLA 2022 | 2022-12-05 |
Proposes plausible sealing: postpone sealing decisions by inserting “maybe-seal” evidence so runtime, not static imprecision, decides whether a value is… | ||
| Purity of an ST monad: full abstraction by semantically typed back-translation | OOPSLA 2022 | 2022-12-05 |
Proves that embedding a pure call-by-value language into an extension with an ST monad is fully abstract: contextual equivalences from the pure language remain… | ||
| Verified Symbolic Execution with Kripke Specification Monads… | ICFP 2022 | 2022-09-11 |
Presents a verified symbolic executor implemented as a Kripke-indexed symbolic specification monad that manipulates deeply embedded assertions, proves… | ||
| Efficient, Provable Local Capability Revocation using Uninitialized Capabilities | POPL 2021 | 2021-01-17 |
Proposes uninitialized capabilities that give write-only access to an uninitialized stack region and require overwriting before any read, implemented with… | ||
| Fully Abstract from Static to Gradual | POPL 2021 | 2021-01-17 |
Proposes that the embedding from static into gradual languages must be fully abstract embedding — it preserves and reflects contextual equivalence — and shows… | ||
| On the Semantic Expressiveness of Recursive Types | POPL 2021 | 2021-01-17 |
Paper proves iso-recursive types, equirecursive types, and a term-level fix are semantically equivalent by constructing three fully abstract compilers… | ||
| Shallowly embedding type theories | TyDe 2020 | 2020-08-23 |
Library in Agda implements a shallow embedding of object type theories as presheaf models parameterized by a small base category, representing… | ||
| nothing matches | ||