Cryptis: Cryptographic Reasoning in Separation Logic.

Amal Ahmed 0001 Amal J. Ahmed 0001 Northeastern University, Khoury College of Computer Sciences, Boston, MA, USA University of Chicago, USA Princeton University, NJ, USA https://www.ccs.neu.edu/home/amal/ http://ttic.uchicago.edu/~amal/ https://orcid.org/0000-0001-7424-572X https://www.wikidata.org/entity/Q60058605 Amal Ahmed Amal J. Ahmed

Arthur Azevedo de Amorim Amal Ahmed 0001 Marco Gaboardi Cryptis: Cryptographic Reasoning in Separation Logic. 2555-2585 2026 10 Proc. ACM Program. Lang. POPL https://doi.org/10.1145/3776730 db/journals/pacmpl/pacmpl10.html#AmorimAG26 streams/journals/pacmpl

Andrew Wagner Olek Gierczak Brianna Marshall John M. Li Amal Ahmed 0001 From Linearity to Borrowing. 3981-4007 2025 9 Proc. ACM Program. Lang. OOPSLA2 https://doi.org/10.1145/3764117 db/journals/pacmpl/pacmpl9.html#WagnerGML025

Arthur Azevedo de Amorim Amal Ahmed 0001 Marco Gaboardi Cryptis: Cryptographic Reasoning in Separation Logic. 2025 February abs/2502.21156 CoRR https://doi.org/10.48550/arXiv.2502.21156 db/journals/corr/corr2502.html#abs-2502-21156 streams/journals/corr

Amal Ahmed 0001 Andreas Rossberg Deian Stefan Conrad Watt Michelle Thalakottur Utilising and Scaling the WebAssembly Semantics (Dagstuhl Seminar 25241). 2025 June 51-68 15 Dagstuhl Reports 6 https://doi.org/10.4230/DagRep.15.6.51 db/journals/dagstuhl-reports/dagstuhl-reports15.html#AhmedRSWT25 streams/journals/dagstuhl-reports

Olek Gierczak Lucy Menon Christos Dimoulas Amal Ahmed 0001 Gradually Typed Languages Should Be Vigilant! 864-892 2024 8 Proc. ACM Program. Lang. OOPSLA1 https://doi.org/10.1145/3649842 db/journals/pacmpl/pacmpl8.html#GierczakMDA24 streams/journals/pacmpl

Andrew Wagner Zachary Eisbach Amal Ahmed 0001 Realistic Realizability: Specifying ABIs You Can Count On. 1249-1278 2024 8 Proc. ACM Program. Lang. OOPSLA2 https://doi.org/10.1145/3689755 https://www.wikidata.org/entity/Q130887629 db/journals/pacmpl/pacmpl8.html#WagnerE024

Michael Fitzgibbons Zoe Paraskevopoulou Noble Mushtak Michelle Thalakottur Jose Sulaiman Manzur Amal Ahmed 0001 RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. 1656-1679 2024 8 Proc. ACM Program. Lang. PLDI https://doi.org/10.1145/3656444 https://www.wikidata.org/entity/Q130952033 db/journals/pacmpl/pacmpl8.html#FitzgibbonsPMTMA24 streams/journals/pacmpl

John M. Li Jon Aytac Philip Johnson-Freyd Amal Ahmed 0001 Steven Holtzen A Nominal Approach to Probabilistic Separation Logic. 55:1-55:14 2024 conf/lics/2024 LICS https://doi.org/10.1145/3661814.3662135 https://www.wikidata.org/entity/Q130807520 db/conf/lics/lics2024.html#LiAJ0H24

Zoe Paraskevopoulou Michael Fitzgibbons Michelle Thalakottur Noble Mushtak Jose Sulaiman Mazur Amal Ahmed 0001 RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. 2024 abs/2401.08287 CoRR https://doi.org/10.48550/arXiv.2401.08287 db/journals/corr/corr2401.html#abs-2401-08287

John M. Li Jon Aytac Philip Johnson-Freyd Amal Ahmed 0001 Steven Holtzen A Nominal Approach to Probabilistic Separation Logic. 2024 abs/2405.06826 CoRR https://doi.org/10.48550/arXiv.2405.06826 db/journals/corr/corr2405.html#abs-2405-06826

John M. Li Amal Ahmed 0001 Steven Holtzen Lilac: A Modal Separation Logic for Conditional Probability. 148-171 2023 7 Proc. ACM Program. Lang. PLDI https://doi.org/10.1145/3591226 https://www.wikidata.org/entity/Q130808716 db/journals/pacmpl/pacmpl7.html#Li0H23

Daniel Patterson 0001 Andrew Wagner Amal Ahmed 0001 Semantic Encapsulation using Linking Types. 14-28 2023 TyDe@ICFP https://doi.org/10.1145/3609027.3609405 conf/icfp/2023tyde db/conf/icfp/tyde2023.html#0001W023

John M. Li Amal Ahmed 0001 Steven Holtzen Lilac: a Modal Separation Logic for Conditional Probability. 2023 abs/2304.01339 CoRR https://doi.org/10.48550/arXiv.2304.01339 db/journals/corr/corr2304.html#abs-2304-01339

Paulette Koronkevich Ramon Rakow Amal Ahmed 0001 William J. Bowman ANF preserves dependent types up to extensional equality. e12 2022 32 J. Funct. Program. https://doi.org/10.1017/S0956796822000090 db/journals/jfp/jfp32.html#KoronkevichRAB22

Daniel Patterson 0001 Noble Mushtak Andrew Wagner Amal Ahmed 0001 Semantic soundness for language interoperability. 609-624 2022 PLDI https://doi.org/10.1145/3519939.3523703 conf/pldi/2022 db/conf/pldi/pldi2022.html#0001MWA22

Daniel Patterson 0001 Noble Mushtak Andrew Wagner Amal Ahmed 0001 Semantic Soundness for Language Interoperability. 2022 abs/2202.13158 CoRR https://arxiv.org/abs/2202.13158 db/journals/corr/corr2202.html#abs-2202-13158

Max S. New Daniel R. Licata Amal Ahmed 0001 Gradual type theory. e21 2021 31 J. Funct. Program. https://doi.org/10.1017/S0956796821000125 db/journals/jfp/jfp31.html#NewLA21

Danel Ahman Amal Ahmed 0001 Sam Lindley Andreas Rossberg Scalable Handling of Effects (Dagstuhl Seminar 21292). 54-81 2021 11 Dagstuhl Reports 6 https://doi.org/10.4230/DagRep.11.6.54 db/journals/dagstuhl-reports/dagstuhl-reports11.html#AhmanALR21

Max S. New Dustin Jamner Amal Ahmed 0001 Graduality and parametricity: together again for the first time. 46:1-46:32 2020 4 POPL Proc. ACM Program. Lang. https://doi.org/10.1145/3371114 https://www.wikidata.org/entity/Q126534775 db/journals/pacmpl/pacmpl4.html#NewJA20

Amal Ahmed 0001 Introduction to the Special Issue on ESOP 2018. 1:1 2020 42 ACM Trans. Program. Lang. Syst. 1 https://doi.org/10.1145/3368252 db/journals/toplas/toplas42.html#Ahmed20

Marco Patrignani Amal Ahmed 0001 Dave Clarke 0001 Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work. 125:1-125:36 2019 51 ACM Comput. Surv. 6 https://doi.org/10.1145/3280984 https://www.wikidata.org/entity/Q128424921 db/journals/csur/csur51.html#PatrignaniAC19

Daniel Patterson 0001 Amal Ahmed 0001 The next 700 compiler correctness theorems (functional pearl). 85:1-85:29 2019 3 Proc. ACM Program. Lang. ICFP https://doi.org/10.1145/3341689 https://www.wikidata.org/entity/Q122704887 db/journals/pacmpl/pacmpl3.html#0001A19

Max S. New Daniel R. Licata Amal Ahmed 0001 Gradual type theory. 15:1-15:31 2019 3 POPL Proc. ACM Program. Lang. https://doi.org/10.1145/3290328 db/journals/pacmpl/pacmpl3.html#NewLA19

Phillip Mates Jamie Perconti Amal Ahmed 0001 Under Control: Compositionally Correct Closure Conversion with Mutable State. 16:1-16:15 2019 PPDP https://doi.org/10.1145/3354166.3354181 conf/ppdp/2019 db/conf/ppdp/ppdp2019.html#MatesPA19

Aaron Weiss Daniel Patterson 0001 Nicholas D. Matsakis Amal Ahmed 0001 Oxide: The Essence of Rust. 2019 abs/1903.00982 CoRR http://arxiv.org/abs/1903.00982 db/journals/corr/corr1903.html#abs-1903-00982

Max S. New Amal Ahmed 0001 Graduality from embedding-projection pairs. 73:1-73:30 2018 2 Proc. ACM Program. Lang. ICFP https://doi.org/10.1145/3236768 db/journals/pacmpl/pacmpl2.html#NewA18

William J. Bowman Youyou Cong Nick Rioux Amal Ahmed 0001 Type-preserving CPS translation of Σ and Π types is not not possible. 22:1-22:33 2018 2 Proc. ACM Program. Lang. POPL https://doi.org/10.1145/3158110 db/journals/pacmpl/pacmpl2.html#BowmanCRA18

Olivier Flückiger Gabriel Scherer Ming-Ho Yee Aviral Goel Amal Ahmed 0001 Jan Vitek Correctness of speculative optimizations with dynamic deoptimization. 49:1-49:28 2018 2 Proc. ACM Program. Lang. POPL https://doi.org/10.1145/3158137 db/journals/pacmpl/pacmpl2.html#FluckigerSYGAV18

Gabriel Scherer Max S. New Nick Rioux Amal Ahmed 0001 Fab ous Interoperability for ML and a Linear Language. 146-162 2018 FoSSaCS https://doi.org/10.1007/978-3-319-89366-2_8 conf/fossacs/2018 db/conf/fossacs/fossacs2018.html#SchererNRA18 William J. Bowman Amal Ahmed 0001 Typed closure conversion for the calculus of constructions. 797-811 2018 PLDI https://doi.org/10.1145/3192366.3192372 https://doi.org/10.1145/3296979.3192372 https://www.wikidata.org/entity/Q128825907 conf/pldi/2018 db/conf/pldi/pldi2018.html#BowmanA18 Amal Ahmed 0001 Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings ESOP Springer 2018 Lecture Notes in Computer Science 10801 978-3-319-89883-4 978-3-319-89884-1 https://doi.org/10.1007/978-3-319-89884-1 db/conf/esop/esop2018.html

Aaron Weiss Daniel Patterson 0001 Amal Ahmed 0001 Rust Distilled: An Expressive Tower of Languages. 2018 abs/1806.02693 CoRR http://arxiv.org/abs/1806.02693 db/journals/corr/corr1806.html#abs-1806-02693

Max S. New Amal Ahmed 0001 Graduality from Embedding-projection Pairs (Extended Version). 2018 abs/1807.02786 CoRR http://arxiv.org/abs/1807.02786 db/journals/corr/corr1807.html#abs-1807-02786

William J. Bowman Amal Ahmed 0001 Typed Closure Conversion for the Calculus of Constructions. 2018 abs/1808.04006 CoRR http://arxiv.org/abs/1808.04006 db/journals/corr/corr1808.html#abs-1808-04006

Max S. New Daniel R. Licata Amal Ahmed 0001 Gradual Type Theory (Extended Version). 2018 abs/1811.02440 CoRR http://arxiv.org/abs/1811.02440 db/journals/corr/corr1811.html#abs-1811-02440

Amal Ahmed 0001 Deepak Garg 0001 Catalin Hritcu Frank Piessens Secure Compilation (Dagstuhl Seminar 18201). 1-30 2018 8 Dagstuhl Reports 5 https://doi.org/10.4230/DagRep.8.5.1 db/journals/dagstuhl-reports/dagstuhl-reports8.html#Ahmed0HP18

Amal Ahmed 0001 Dustin Jamner Jeremy G. Siek Philip Wadler Theorems for free for free: parametricity, with and without types. 39:1-39:28 2017 1 Proc. ACM Program. Lang. ICFP https://doi.org/10.1145/3110283 db/journals/pacmpl/pacmpl1.html#AhmedJSW17

Daniel Patterson 0001 Jamie Perconti Christos Dimoulas Amal Ahmed 0001 FunTAL: reasonably mixing a functional language with assembly. 495-509 2017 PLDI https://doi.org/10.1145/3062341.3062347 https://doi.org/10.1145/3140587.3062347 https://www.wikidata.org/entity/Q60142670 conf/pldi/2017 db/conf/pldi/pldi2017.html#PattersonPDA17 Daniel Patterson 0001 Amal Ahmed 0001 Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. 12:1-12:15 2017 SNAPL https://doi.org/10.4230/LIPIcs.SNAPL.2017.12 conf/snapl/2017 db/conf/snapl/snapl2017.html#PattersonA17

Gabriel Scherer Max S. New Nicholas Rioux Amal Ahmed 0001 FabULous Interoperability for ML and a Linear Language. 2017 abs/1707.04984 CoRR http://arxiv.org/abs/1707.04984 db/journals/corr/corr1707.html#SchererNRA17

Olivier Flückiger Gabriel Scherer Ming-Ho Yee Aviral Goel Amal Ahmed 0001 Jan Vitek Correctness of Speculative Optimizations with Dynamic Deoptimization. 2017 abs/1711.03050 CoRR http://arxiv.org/abs/1711.03050 db/journals/corr/corr1711.html#abs-1711-03050

Daniel Patterson 0001 Jamie Perconti Christos Dimoulas Amal Ahmed 0001 FunTAL: Reasonably Mixing a Functional Language with Assembly. 2017 abs/1711.03871 CoRR http://arxiv.org/abs/1711.03871 db/journals/corr/corr1711.html#abs-1711-03871

Daniel Patterson 0001 Amal Ahmed 0001 Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. 2017 abs/1711.04559 CoRR http://arxiv.org/abs/1711.04559 db/journals/corr/corr1711.html#abs-1711-04559

Max S. New William J. Bowman Amal Ahmed 0001 Fully abstract compilation via universal embedding. 103-116 2016 ICFP https://doi.org/10.1145/2951913.2951941 https://doi.org/10.1145/3022670.2951941 conf/icfp/2016 db/conf/icfp/icfp2016.html#NewBA16 Amal Ahmed 0001 Compositional Compiler Verification for a Multi-Language World. 1:1-1:1 2016 FSCD https://doi.org/10.4230/LIPIcs.FSCD.2016.1 conf/rta/2016 db/conf/rta/fscd2016.html#Ahmed16 William J. Bowman Amal Ahmed 0001 Noninterference for free. 101-113 2015 ICFP https://doi.org/10.1145/2784731.2784733 https://doi.org/10.1145/2858949.2784733 https://www.wikidata.org/entity/Q60142672 conf/icfp/2015 db/conf/icfp/icfp2015.html#BowmanA15 Amal Ahmed 0001 Verified Compilers for a Multi-Language World. 15-31 2015 SNAPL https://doi.org/10.4230/LIPIcs.SNAPL.2015.15 conf/snapl/2015 db/conf/snapl/snapl2015.html#Ahmed15 James T. Perconti Amal Ahmed 0001 Verifying an Open Compiler Using Multi-language Semantics. 128-148 2014 ESOP https://doi.org/10.1007/978-3-642-54833-8_8 https://www.wikidata.org/entity/Q60142674 conf/esop/2014 db/conf/esop/esop2014.html#PercontiA14 James Cheney Amal Ahmed 0001 Umut A. Acar Database Queries that Explain their Work. 271-282 2014 PPDP https://doi.org/10.1145/2643135.2643143 https://www.wikidata.org/entity/Q60142673 conf/ppdp/2014 db/conf/ppdp/ppdp2014.html#CheneyAA14

James Cheney Amal Ahmed 0001 Umut A. Acar Database Queries that Explain their Work. 2014 abs/1408.1675 CoRR http://arxiv.org/abs/1408.1675 db/journals/corr/corr1408.html#CheneyAA14

Umut A. Acar Amal Ahmed 0001 James Cheney Roly Perera A core calculus for provenance. 919-969 2013 21 J. Comput. Secur. 6 https://doi.org/10.3233/JCS-130487 https://www.wikidata.org/entity/Q60142676 db/journals/jcs/jcs21.html#AcarACP13

Aaron Joseph Turon Jacob Thamsborg Amal Ahmed 0001 Lars Birkedal Derek Dreyer Logical relations for fine-grained concurrency. 343-356 2013 POPL https://doi.org/10.1145/2429069.2429111 https://doi.org/10.1145/2480359.2429111 https://www.wikidata.org/entity/Q60142677 conf/popl/2013 db/conf/popl/popl2013.html#TuronTABD13

Umut A. Acar Amal Ahmed 0001 James Cheney Roly Perera A Core Calculus for Provenance. 2013 CoRR http://arxiv.org/abs/1310.6299 abs/1310.6299 db/journals/corr/corr1310.html#AcarACP13

Umut A. Acar Amal Ahmed 0001 James Cheney Roly Perera A Core Calculus for Provenance. 410-429 2012 POST https://doi.org/10.1007/978-3-642-28641-4_22 https://www.wikidata.org/entity/Q60142679 conf/post/2012 db/conf/post/post2012.html#AcarACP12

Derek Dreyer Amal Ahmed 0001 Lars Birkedal Logical Step-Indexed Logical Relations https://doi.org/10.2168/LMCS-7(2:16)2011 http://arxiv.org/abs/1103.0510 2011 Log. Methods Comput. Sci. 7 2 db/journals/lmcs/lmcs7.html#abs-1103-0510

James Cheney Amal Ahmed 0001 Umut A. Acar Provenance as dependency analysis. 1301-1337 2011 21 Math. Struct. Comput. Sci. 6 https://doi.org/10.1017/S0960129511000211 https://www.wikidata.org/entity/Q60142684 db/journals/mscs/mscs21.html#CheneyAA11

Amal Ahmed 0001 Matthias Blume An equivalence-preserving CPS translation via multi-language semantics. 431-444 2011 ICFP https://doi.org/10.1145/2034773.2034830 https://doi.org/10.1145/2034574.2034830 https://www.wikidata.org/entity/Q60142680 conf/icfp/2011 db/conf/icfp/icfp2011.html#AhmedB11 Amal Ahmed 0001 Robert Bruce Findler Jeremy G. Siek Philip Wadler Blame for all. 201-214 2011 POPL https://doi.org/10.1145/1926385.1926409 https://doi.org/10.1145/1925844.1926409 https://www.wikidata.org/entity/Q60142685 conf/popl/2011 db/conf/popl/popl2011.html#AhmedFSW11

Amal Ahmed 0001 Andrew W. Appel Christopher D. Richards Kedar N. Swadi Gang Tan Daniel C. Wang Semantic foundations for typed assembly languages. 2010 32 ACM Trans. Program. Lang. Syst. 3 https://doi.org/10.1145/1709093.1709094 https://www.wikidata.org/entity/Q60142686 db/journals/toplas/toplas32.html#AhmedARSTW10 7:1-7:67

Amal Ahmed 0001 Nick Benton Lars Birkedal Martin Hofmann 0001 Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010 Modelling, Controlling and Reasoning About State 10351 2010 Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany Dagstuhl Seminar Proceedings db/conf/dagstuhl/P10351.html http://drops.dagstuhl.de/portals/10351/ Amal Ahmed 0001 Nick Benton Lars Birkedal Martin Hofmann 0001 10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. 2010 Modelling, Controlling and Reasoning About State http://drops.dagstuhl.de/opus/volltexte/2010/2811/ conf/dagstuhl/2010P10351 db/conf/dagstuhl/P10351.html#AhmedBB010 Amal Ahmed 0001 Nick Benton Lars Birkedal Martin Hofmann 0001 10351 Executive Summary - Modelling, Controlling and Reasoning About State. 2010 Modelling, Controlling and Reasoning About State http://drops.dagstuhl.de/opus/volltexte/2010/2810/ conf/dagstuhl/2010P10351 db/conf/dagstuhl/P10351.html#AhmedBB010a Amal Ahmed 0001 Robert Bruce Findler Jacob Matthews Philip Wadler Blame for all. 1-13 2009 STOP@ECOOP https://doi.org/10.1145/1570506.1570507 https://www.wikidata.org/entity/Q60142687 conf/ecoop/2009stop db/conf/ecoop/stop2009.html#AhmedFMW09 Derek Dreyer Amal Ahmed 0001 Lars Birkedal Logical Step-Indexed Logical Relations. 71-80 2009 LICS https://doi.org/10.1109/LICS.2009.34 https://doi.ieeecomputersociety.org/10.1109/LICS.2009.34 https://www.wikidata.org/entity/Q60142688 conf/lics/2009 db/conf/lics/lics2009.html#DreyerAB09 Amal Ahmed 0001 Derek Dreyer Andreas Rossberg State-dependent representation independence. 340-353 2009 POPL https://doi.org/10.1145/1480881.1480925 https://doi.org/10.1145/1594834.1480925 https://www.wikidata.org/entity/Q60142689 conf/popl/2009 db/conf/popl/popl2009.html#AhmedDR09 Andrew Kennedy Amal Ahmed 0001 Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009 TLDI ACM 2009 db/conf/tldi/tldi2009.html 978-1-60558-420-1 http://dl.acm.org/citation.cfm?id=1481861 Jacob Matthews Amal Ahmed 0001 Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!. 16-31 2008 ESOP https://doi.org/10.1007/978-3-540-78739-6_2 https://www.wikidata.org/entity/Q60142691 conf/esop/2008 db/conf/esop/esop2008.html#MatthewsA08 Amal Ahmed 0001 Matthias Blume Typed closure conversion preserves observational equivalence. 157-168 2008 ICFP https://doi.org/10.1145/1411204.1411227 https://doi.org/10.1145/1411203.1411227 https://www.wikidata.org/entity/Q60142692 conf/icfp/2008 db/conf/icfp/icfp2008.html#AhmedB08 Umut A. Acar Amal Ahmed 0001 Matthias Blume Imperative self-adjusting computation. 309-322 2008 conf/popl/2008 POPL https://doi.org/10.1145/1328438.1328476 https://doi.org/10.1145/1328897.1328476 https://www.wikidata.org/entity/Q60142690 db/conf/popl/popl2008.html#AcarAB08 Amal Ahmed 0001 Nick Benton Martin Hofmann 0001 Greg Morrisett Types, Logics and Semantics for State, 03.02. - 08.02.2008 Types, Logics and Semantics for State 08061 2008 db/conf/dagstuhl/P8061.html http://drops.dagstuhl.de/portals/08061/ Dagstuhl Seminar Proceedings Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany Amal Ahmed 0001 Nick Benton Martin Hofmann 0001 Greg Morrisett 08061 Executive Summary -- Types, Logics and Semantics for State. 2008 Types, Logics and Semantics for State http://drops.dagstuhl.de/opus/volltexte/2008/1426 conf/dagstuhl/2008P8061 db/conf/dagstuhl/P8061.html#AhmedBHM08 Amal Ahmed 0001 Nick Benton Martin Hofmann 0001 Greg Morrisett 08061 Abstracts Collection -- Types, Logics and Semantics for State. 2008 Types, Logics and Semantics for State http://drops.dagstuhl.de/opus/volltexte/2008/1428 conf/dagstuhl/2008P8061 db/conf/dagstuhl/P8061.html#AhmedBHM08a

James Cheney Umut A. Acar Amal Ahmed 0001 Provenance Traces http://arxiv.org/abs/0812.0564 2008 CoRR abs/0812.0564 db/journals/corr/corr0812.html#abs-0812-0564

Amal Ahmed 0001 Matthew Fluet Greg Morrisett L<sup>3</sup>: A Linear Language with Locations. 397-449 2007 77 Fundam. Informaticae 4 http://content.iospress.com/articles/fundamenta-informaticae/fi77-4-06 db/journals/fuin/fuin77.html#AhmedFM07

James Cheney Amal Ahmed 0001 Umut A. Acar Provenance as Dependency Analysis. 138-152 2007 conf/dbpl/2007 DBPL https://doi.org/10.1007/978-3-540-75987-4_10 db/conf/dbpl/dbpl2007.html#CheneyAA07 Aleksandar Nanevski Amal Ahmed 0001 Greg Morrisett Lars Birkedal Abstract Predicates and Mutable ADTs in Hoare Type Theory. 189-204 2007 conf/esop/2007 ESOP https://doi.org/10.1007/978-3-540-71316-6_14 db/conf/esop/esop2007.html#NanevskiAMB07

James Cheney Amal Ahmed 0001 Umut A. Acar Provenance as Dependency Analysis http://arxiv.org/abs/0708.2173 2007 CoRR abs/0708.2173 db/journals/corr/corr0708.html#abs-0708-2173

Matthew Fluet Greg Morrisett Amal J. Ahmed 0001 Linear Regions Are All You Need. 7-21 2006 conf/esop/2006 ESOP https://doi.org/10.1007/11693024_2 https://www.wikidata.org/entity/Q60142693 db/conf/esop/esop2006.html#FluetMA06 Amal J. Ahmed 0001 Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. 69-83 2006 conf/esop/2006 ESOP https://doi.org/10.1007/11693024_6 db/conf/esop/esop2006.html#Ahmed06 Amal J. Ahmed 0001 Matthew Fluet Greg Morrisett A step-indexed model of substructural state. 78-91 2005 conf/icfp/2005 ICFP https://doi.org/10.1145/1086365.1086376 https://doi.org/10.1145/1090189.1086376 https://www.wikidata.org/entity/Q60142694 db/conf/icfp/icfp2005.html#AhmedFM05 Greg Morrisett Amal J. Ahmed 0001 Matthew Fluet L<sup>3</sup>: A Linear Language with Locations. 293-307 https://doi.org/10.1007/11417170_22 2005 conf/tlca/2005 TLCA db/conf/tlca/tlca2005.html#MorrisettAF05 Amal J. Ahmed 0001 Limin Jia 0001 David Walker 0001 Reasoning about Hierarchical Storage. 33-44 2003 conf/lics/2003 LICS https://doi.org/10.1109/LICS.2003.1210043 https://doi.ieeecomputersociety.org/10.1109/LICS.2003.1210043 db/conf/lics/lics2003.html#AhmedJW03 Amal J. Ahmed 0001 David Walker 0001 The logical approach to stack typing. 74-85 2003 conf/tldi/2003 TLDI https://doi.org/10.1145/604174.604185 https://doi.org/10.1145/640136.604185 db/conf/tldi/tldi2003.html#AhmedW03 Amal J. Ahmed 0001 Andrew W. Appel Roberto Virga A Stratified Semantics of General References A Stratified Semantics of General References. 75- 2002 conf/lics/2002 LICS https://doi.org/10.1109/LICS.2002.1029818 https://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029818 db/conf/lics/lics2002.html#AhmedAV02 Umut A. Acar Danel Ahman Arthur Azevedo de Amorim Andrew W. Appel Jon Aytac Nick Benton Lars Birkedal Matthias Blume William J. Bowman James Cheney Dave Clarke 0001 Youyou Cong Christos Dimoulas Derek Dreyer Zachary Eisbach Robert Bruce Findler Michael Fitzgibbons Olivier Flückiger Matthew Fluet Marco Gaboardi Deepak Garg 0001 Olek Gierczak Aviral Goel Martin Hofmann 0001 Steven Holtzen Catalin Hritcu Dustin Jamner Limin Jia 0001 Philip Johnson-Freyd Andrew Kennedy Paulette Koronkevich John M. Li Daniel R. Licata Sam Lindley Jose Sulaiman Manzur Brianna Marshall Phillip Mates Nicholas D. Matsakis Jacob Matthews Jose Sulaiman Mazur Lucy Menon J. Gregory MorrisettGreg Morrisett Noble Mushtak Aleksandar Nanevski Max S. New Zoe Paraskevopoulou Marco Patrignani Daniel Patterson 0001 James T. PercontiJamie Perconti Roly Perera Frank Piessens Ramon Rakow Christopher D. Richards Nicholas Rioux Nick Rioux Andreas Rossberg Gabriel Scherer Jeremy G. Siek Deian Stefan Kedar N. Swadi Gang Tan Michelle Thalakottur Jacob Thamsborg Aaron TuronAaron Joseph Turon Roberto Virga Jan Vitek Philip Wadler Andrew Wagner David Walker 0001 Daniel C. Wang Conrad Watt Aaron Weiss Ming-Ho Yee