Amin Timany
where else to find them
what they talk about
all 7 in the filters
where they keep going back
all 5 in the filters
on a stage with
all 25 in the filters
who talks about the same things
- Lars Birkedal35 talks
- Simon Oddershede Gregersen9 talks
- Léon Gondelman4 talks
- Michael Sammler16 talks
- Jonas Kastberg Hinrichsen6 talks
- Joseph Tassarotti20 talks
| title | conference | date |
|---|---|---|
| Reasoning about Weak Isolation Levels in Separation Logic | ICFP 2025 | 2025-10-12 |
Paper formalizes three weak isolation levels for key-value transactions and mechanizes them in Rocq on Iris, giving atomic-style separation-logic specs for… | ||
| The Logical Essence of Well-Bracketed Control Flow | POPL 2024 | 2024-01-14 |
First Hoare-style separation logic for well-bracketed control flow that proves the closure-from-example always returns one when called with a function that… | ||
| Modular Denotational Semantics for Effects with Guarded Interaction Trees | POPL 2024 | 2024-01-14 |
Introduces guarded interaction trees as a denotational domain for higher-order effects, fully formalized in Coq/Iris formalization with reusable artifacts… | ||
| Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intension... | POPL 2024 | 2024-01-14 |
Introduces Trillium as a language-agnostic separation-logic framework that proves intensional refinements between program traces and labeled transition models… | ||
| Verifying Reliable Network Components in a Distributed Separation Logic with Dep... | ICFP 2023 | 2023-09-04 |
Claims a verified reliable client–server communication stack implemented in an OCaml-like language (about 300–400 lines of code) that runs over UDP and… | ||
| VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…) | PLDI 2023 | 2023-06-17 |
Formalises a substantial fragment of Arm FF‑A as a toy ISA with hypercalls and develops VMSL separation logic to reason about VM-to-VM shared pages and handoff… | ||
| 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… | ||
| A Verified Pipeline from a Specification Language to Optimized, Safe Rust | CoqPL 2022 | 2022-01-22 |
A verified pipeline converts hacspec executable specs to optimized, safe Rust by adding a Coq backend for hacspec, synthesizing low-level code with Fiat… | ||
| Reasoning in Higher-Order Concurrent Separation Logic | POPL 2021 | 2021-01-17 |
Iris program logic is a higher-order concurrent separation logic that produces a tailored program logic from an operational semantics and an adequacy theorem… | ||
| Distributed Causal Memory for Higher-Order Distributed Separation Logic | POPL 2021 | 2021-01-17 |
Presents the first full specification and machine-checked verification of a causally-consistent distributed database implementation and client libraries… | ||
| 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… | ||
| Mechanized Logical Relations for Termination-Insensitive Noninterference | POPL 2021 | 2021-01-17 |
Paper proves that a rich information‑flow type system (recursive and existential types, System F impredicative polymorphism, label polymorphism, higher‑order… | ||
| Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris | ICFP 2020 | 2020-08-23 |
Presents a semantics-first proof that adds guardedness to DOT via a step-indexed logical relation built in Iris, yielding gDOT that models impredicative… | ||
| nothing matches | ||