A Stratified Semantics of General References A Stratified Semantics of General References. - Amal J. Ahmed 001; Andrew W. Appel; Roberto Virga (LICS, 2002)

Reasoning about Hierarchical Storage. - Amal J. Ahmed 001; Limin Jia 001; David Walker 001 (LICS, 2003)

The logical approach to stack typing. - Amal J. Ahmed 001; David Walker 001 (TLDI, 2003)

A step-indexed model of substructural state. - Amal J. Ahmed 001; Matthew Fluet; Greg Morrisett (ICFP, 2005)

Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. - Amal J. Ahmed 001 (ESOP, 2006)

Linear Regions Are All You Need. - Matthew Fluet; Greg Morrisett; Amal J. Ahmed 001 (ESOP, 2006)

Abstract Predicates and Mutable ADTs in Hoare Type Theory. - Aleksandar Nanevski; Amal Ahmed 001; Greg Morrisett; Lars Birkedal (ESOP, 2007)

L3: A Linear Language with Locations. - Amal Ahmed 001; Matthew Fluet; Greg Morrisett (Fundam. Informaticae, 2007)

08061 Executive Summary – Types, Logics and Semantics for State. - Amal Ahmed 001; Nick Benton; Martin Hofmann 001; Greg Morrisett (Types, Logics and Semantics for State, 2008)

08061 Abstracts Collection – Types, Logics and Semantics for State. - Amal Ahmed 001; Nick Benton; Martin Hofmann 001; Greg Morrisett (Types, Logics and Semantics for State, 2008)

Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!. - Jacob Matthews; Amal Ahmed 001 (ESOP, 2008)

Typed closure conversion preserves observational equivalence. - Amal Ahmed 001; Matthias Blume (ICFP, 2008)

Imperative self-adjusting computation. - Umut A. Acar; Amal Ahmed 001; Matthias Blume (POPL, 2008)

Provenance Traces - James Cheney; Umut A. Acar; Amal Ahmed 001 (CoRR, 2008)

Blame for all. - Amal Ahmed 001; Robert Bruce Findler; Jacob Matthews; Philip Wadler (STOP@ECOOP, 2009)

State-dependent representation independence. - Amal Ahmed 001; Derek Dreyer; Andreas Rossberg (POPL, 2009)

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. - Amal Ahmed 001; Nick Benton; Lars Birkedal; Martin Hofmann 001 (Modelling, Controlling and Reasoning About State, 2010)

10351 Executive Summary - Modelling, Controlling and Reasoning About State. - Amal Ahmed 001; Nick Benton; Lars Birkedal; Martin Hofmann 001 (Modelling, Controlling and Reasoning About State, 2010)

Semantic foundations for typed assembly languages. - Amal Ahmed 001; Andrew W. Appel; Christopher D. Richards; Kedar N. Swadi; Gang Tan; Daniel C. Wang (ACM Trans. Program. Lang. Syst., 2010)

An equivalence-preserving CPS translation via multi-language semantics. - Amal Ahmed 001; Matthias Blume (ICFP, 2011)

Blame for all. - Amal Ahmed 001; Robert Bruce Findler; Jeremy G. Siek; Philip Wadler (POPL, 2011)

Logical Step-Indexed Logical Relations - Derek Dreyer; Amal Ahmed 001; Lars Birkedal (Log. Methods Comput. Sci., 2011)

Provenance as dependency analysis. - James Cheney; Amal Ahmed 001; Umut A. Acar (Math. Struct. Comput. Sci., 2011)

Logical relations for fine-grained concurrency. - Aaron Joseph Turon; Jacob Thamsborg; Amal Ahmed 001; Lars Birkedal; Derek Dreyer (POPL, 2013)

A core calculus for provenance. - Umut A. Acar; Amal Ahmed 001; James Cheney; Roly Perera (J. Comput. Secur., 2013)

Verifying an Open Compiler Using Multi-language Semantics. - James T. Perconti; Amal Ahmed 001 (ESOP, 2014)

Database Queries that Explain their Work. - James Cheney; Amal Ahmed 001; Umut A. Acar (PPDP, 2014)

Noninterference for free. - William J. Bowman; Amal Ahmed 001 (ICFP, 2015)

Verified Compilers for a Multi-Language World. - Amal Ahmed 001 (SNAPL, 2015)

Fully abstract compilation via universal embedding. - Max S. New; William J. Bowman; Amal Ahmed 001 (ICFP, 2016)

Compositional Compiler Verification for a Multi-Language World. - Amal Ahmed 001 (FSCD, 2016)

FunTAL: reasonably mixing a functional language with assembly. - Daniel Patterson 001; Jamie Perconti; Christos Dimoulas; Amal Ahmed 001 (PLDI, 2017)

Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. - Daniel Patterson 001; Amal Ahmed 001 (SNAPL, 2017)

FabULous Interoperability for ML and a Linear Language. - Gabriel Scherer; Max S. New; Nicholas Rioux; Amal Ahmed 001 (CoRR, 2017)

Theorems for free for free: parametricity, with and without types. - Amal Ahmed 001; Dustin Jamner; Jeremy G. Siek; Philip Wadler (Proc. ACM Program. Lang., 2017)

Fab ous Interoperability for ML and a Linear Language. - Gabriel Scherer; Max S. New; Nick Rioux; Amal Ahmed 001 (FoSSaCS, 2018)

Typed closure conversion for the calculus of constructions. - William J. Bowman; Amal Ahmed 001 (PLDI, 2018)

Rust Distilled: An Expressive Tower of Languages. - Aaron Weiss; Daniel Patterson 001; Amal Ahmed 001 (CoRR, 2018)

Graduality from Embedding-projection Pairs (Extended Version). - Max S. New; Amal Ahmed 001 (CoRR, 2018)

Gradual Type Theory (Extended Version). - Max S. New; Daniel R. Licata; Amal Ahmed 001 (CoRR, 2018)

Secure Compilation (Dagstuhl Seminar 18201). - Amal Ahmed 001; Deepak Garg 001; Catalin Hritcu; Frank Piessens (Dagstuhl Reports, 2018)

Type-preserving CPS translation of Σ and Π types is not not possible. - William J. Bowman; Youyou Cong; Nick Rioux; Amal Ahmed 001 (Proc. ACM Program. Lang., 2018)

Correctness of speculative optimizations with dynamic deoptimization. - Olivier Flückiger; Gabriel Scherer; Ming-Ho Yee; Aviral Goel; Amal Ahmed 001; Jan Vitek (Proc. ACM Program. Lang., 2018)

Graduality from embedding-projection pairs. - Max S. New; Amal Ahmed 001 (Proc. ACM Program. Lang., 2018)

Under Control: Compositionally Correct Closure Conversion with Mutable State. - Phillip Mates; Jamie Perconti; Amal Ahmed 001 (PPDP, 2019)

Oxide: The Essence of Rust. - Aaron Weiss; Daniel Patterson 001; Nicholas D. Matsakis; Amal Ahmed 001 (CoRR, 2019)

Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work. - Marco Patrignani; Amal Ahmed 001; Dave Clarke 001 (ACM Comput. Surv., 2019)

The next 700 compiler correctness theorems (functional pearl). - Daniel Patterson 001; Amal Ahmed 001 (Proc. ACM Program. Lang., 2019)

Gradual type theory. - Max S. New; Daniel R. Licata; Amal Ahmed 001 (Proc. ACM Program. Lang., 2019)

Graduality and parametricity: together again for the first time. - Max S. New; Dustin Jamner; Amal Ahmed 001 (Proc. ACM Program. Lang., 2020)

Introduction to the Special Issue on ESOP 2018. - Amal Ahmed 001 (ACM Trans. Program. Lang. Syst., 2020)

Scalable Handling of Effects (Dagstuhl Seminar 21292). - Danel Ahman; Amal Ahmed 001; Sam Lindley; Andreas Rossberg (Dagstuhl Reports, 2021)

Semantic soundness for language interoperability. - Daniel Patterson 001; Noble Mushtak; Andrew Wagner; Amal Ahmed 001 (PLDI, 2022)

ANF preserves dependent types up to extensional equality. - Paulette Koronkevich; Ramon Rakow; Amal Ahmed 001; William J. Bowman (J. Funct. Program., 2022)

Semantic Encapsulation using Linking Types. - Daniel Patterson 001; Andrew Wagner; Amal Ahmed 001 (TyDe@ICFP, 2023)

Lilac: A Modal Separation Logic for Conditional Probability. - John M. Li; Amal Ahmed 001; Steven Holtzen (Proc. ACM Program. Lang., 2023)

A Nominal Approach to Probabilistic Separation Logic. - John M. Li; Jon Aytac; Philip Johnson-Freyd; Amal Ahmed 001; Steven Holtzen (LICS, 2024)

RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. - Zoe Paraskevopoulou; Michael Fitzgibbons; Michelle Thalakottur; Noble Mushtak; Jose Sulaiman Mazur; Amal Ahmed 001 (CoRR, 2024)

RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. - Michael Fitzgibbons; Zoe Paraskevopoulou; Noble Mushtak; Michelle Thalakottur; Jose Sulaiman Manzur; Amal Ahmed 001 (Proc. ACM Program. Lang., 2024)

Gradually Typed Languages Should Be Vigilant! - Olek Gierczak; Lucy Menon; Christos Dimoulas; Amal Ahmed 001 (Proc. ACM Program. Lang., 2024)

Realistic Realizability: Specifying ABIs You Can Count On. - Andrew Wagner; Zachary Eisbach; Amal Ahmed 001 (Proc. ACM Program. Lang., 2024)

Cryptis: Cryptographic Reasoning in Separation Logic. - Arthur Azevedo de Amorim; Amal Ahmed 001; Marco Gaboardi (CoRR, 2025)