Amal Ahmed
where else to find them
no profile links on file
what they talk about
all 7 in the filters
where they keep going back
all 13 in the filters
on a stage with
all 28 in the filters
who talks about the same things
- Lars Birkedal35 talks
- Deepak Garg18 talks
- John M. Li4 talks
- Neel Krishnaswami10 talks
- Michael Sammler16 talks
- Nadia Polikarpova24 talks
| title | conference | date |
|---|---|---|
| Specifying ABIs with Realizability and Type-Preserving Compilation | PriSC 2026 | 2026-01-11 |
Claims a Realizability model for RichWasm that interprets source types as sets of WebAssembly configurations so a type-preserving compiler yields a memory-safe… | ||
| 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… | ||
| From Linearity to Borrowing | OOPSLA 2025 | 2025-10-16 |
Builds a lightweight borrowing extension on a linear lambda calculus and implements the API as untyped terms validated by logic, not new runtime primitives… | ||
| Gradually Typed Languages Should Be Vigilant! | OOPSLA 2024 | 2024-10-20 |
Defines vigilance as a semantic criterion that checks whether runtime enforcement preserves the full run-time typing history; implements it by instrumenting… | ||
| Realistic Realizability: Specifying ABIs You Can Count On | OOPSLA 2024 | 2024-10-20 |
Proposes using realistic realizability models to specify ABIs by connecting high-level types to concrete target code and builds a graph-based separation logic… | ||
| An Incremental Approach to the Semantics of Borrowing | HOPE 2024 | 2024-09-02 |
Presents a core, extensible borrow calculus built incrementally: start from a linear call-by-push-value core, add immutable borrows, lifetimes, mutable… | ||
| RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly | PLDI 2024 | 2024-06-24 |
RichWasm is a richly typed IR on top of WebAssembly that adds capability types, separate unrestricted (GC) and linear (unique-owner) memories, and… | ||
| All the Binaries Together: A Semantic Approach to Application Binary Interfaces | PriSC 2024 | 2024-01-20 |
Proposes a concrete semantic ABI that maps a functional source language to a C-ish, reference-counted target using realizability models and separation logic to… | ||
| RichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssem... | WAW 2024 | 2024-01-15 |
RichWasm is a higher-level WebAssembly dialect with a capability-based type system that enforces fine-grained, cross-language shared-memory safety: it models… | ||
| Towards a Categorical Model of the Lilac Separation Logic | LAFI 2024 | 2024-01-14 |
Constructs two categories—a probabilistic “sheaf/topos–style” category and a nominal-style category—and proves they are equivalent, so Lilac’s independent… | ||
| All the Languages Together | OOPSLA 2023 | 2023-10-23 |
Proposes a proof technique that builds a semantic intermediate representation (logical relations of source types as sets of target terms) to verify FFI glue… | ||
| Formal semantics for multi-language programs | PWLConf 2023 | 2023-09-21 |
Claims that a 2007 recipe gives a practical operational semantics for linking two source languages by adding typed boundaries and two concrete mechanisms: the… | ||
| Formal semantics for multi-language programs | Strange Loop 2023 | 2023-09-21 |
Presents a concrete recipe: add typed boundaries between two languages, run each fragment with its own operational semantics, and convert values at the… | ||
| Semantic Encapsulation using Linking Types | TyDe 2023 | 2023-09-04 |
Presents a concrete mechanism that lets a pure language safely link to foreign code by adding linking types that describe C‑like behaviors, proving soundness… | ||
| Fireside chat | ICFP 2023 | 2023-09-04 |
History of Rust traces concrete choices: adoption of explicit lifetimes evolving into non-lexical lifetimes to handle lookup/mutation patterns, planning… | ||
| Lilac: A Modal Separation Logic for Conditional Probability | PLDI 2023 | 2023-06-17 |
Lilac presents a separation logic that models probability spaces as heap-like resources and defines an independent combination operator that interprets… | ||
| Semantic Intermediate Representations for Sound Language Interoperability | PriSC 2023 | 2023-01-21 |
Claim: build semantic IRs — logical relations that map each source type to a set of target terms — to prove interoperability after compilation. Implementation… | ||
| Introduction | PLMW @ POPL 2023 | 2023-01-17 |
PLMW emphasizes two concrete goals: get a grasp of what PL research is producing and meet people who do it. The program has 74 papers from 275 submissions, a… | ||
| New foundations for probabilistic separation logic | LAFI 2023 | 2023-01-15 |
Proposes a new separation-logic semantics where propositions are sets of probability spaces and heaps are replaced by probability-space fragments combined with… | ||
| Welcome to POPL'23 | POPL 2023 | 2023-01-15 |
Conference opens on the 50th POPL with over 500 in-person attendees (700 counting co-located events) and a technical program of 74 papers from 275 submissions… | ||
| Managing your Research, your Advisor, your PhD | PLMW @ ICFP 2020 | 2020-08-23 |
Prioritize advisor fit over school prestige and choose projects the group actually cares about; start with a starter project that teaches needed skills and aim… | ||
| All the Languages Together | Strange Loop 2018 | 2018-09-26 |
Proposes that safe multi-language composition requires concrete annotations and compilers not vague promises: add linking types (e.g. linear types for… | ||
| nothing matches | ||