Amal Ahmed

Orcid: 0000-0001-7424-572X

Affiliations:
  • Northeastern University, Khoury College of Computer Sciences, Boston, MA, USA
  • University of Chicago, USA (former)
  • Princeton University, NJ, USA (PhD 2004)


According to our database1, Amal Ahmed authored at least 57 papers between 2002 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly.
CoRR, 2024

2023
Lilac: A Modal Separation Logic for Conditional Probability.
Proc. ACM Program. Lang., 2023

Semantic Encapsulation using Linking Types.
Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development, 2023

2022
ANF preserves dependent types up to extensional equality.
J. Funct. Program., 2022

Semantic soundness for language interoperability.
Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021
Scalable Handling of Effects (Dagstuhl Seminar 21292).
Dagstuhl Reports, 2021

2020
Introduction to the Special Issue on ESOP 2018.
ACM Trans. Program. Lang. Syst., 2020

Graduality and parametricity: together again for the first time.
Proc. ACM Program. Lang., 2020

2019
Gradual type theory.
Proc. ACM Program. Lang., 2019

The next 700 compiler correctness theorems (functional pearl).
Proc. ACM Program. Lang., 2019

Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work.
ACM Comput. Surv., 2019

Oxide: The Essence of Rust.
CoRR, 2019

Under Control: Compositionally Correct Closure Conversion with Mutable State.
Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

2018
Graduality from embedding-projection pairs.
Proc. ACM Program. Lang., 2018

Correctness of speculative optimizations with dynamic deoptimization.
Proc. ACM Program. Lang., 2018

Type-preserving CPS translation of Σ and Π types is not not possible.
Proc. ACM Program. Lang., 2018

Secure Compilation (Dagstuhl Seminar 18201).
Dagstuhl Reports, 2018

Gradual Type Theory (Extended Version).
CoRR, 2018

Graduality from Embedding-projection Pairs (Extended Version).
CoRR, 2018

Rust Distilled: An Expressive Tower of Languages.
CoRR, 2018

Typed closure conversion for the calculus of constructions.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Fab ous Interoperability for ML and a Linear Language.
Proceedings of the Foundations of Software Science and Computation Structures, 2018

2017
Theorems for free for free: parametricity, with and without types.
Proc. ACM Program. Lang., 2017

FabULous Interoperability for ML and a Linear Language.
CoRR, 2017

Linking Types for Multi-Language Software: Have Your Cake and Eat It Too.
Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

FunTAL: reasonably mixing a functional language with assembly.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

2016
Compositional Compiler Verification for a Multi-Language World.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Fully abstract compilation via universal embedding.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015
Verified Compilers for a Multi-Language World.
Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Noninterference for free.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

2014
Database Queries that Explain their Work.
Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, 2014

Verifying an Open Compiler Using Multi-language Semantics.
Proceedings of the Programming Languages and Systems, 2014

2013
A core calculus for provenance.
J. Comput. Secur., 2013

Logical relations for fine-grained concurrency.
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

2011
Provenance as dependency analysis.
Math. Struct. Comput. Sci., 2011

Logical Step-Indexed Logical Relations
Log. Methods Comput. Sci., 2011

Blame for all.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

An equivalence-preserving CPS translation via multi-language semantics.
Proceedings of the Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, 2011

2010
Semantic foundations for typed assembly languages.
ACM Trans. Program. Lang. Syst., 2010

10351 Executive Summary - Modelling, Controlling and Reasoning About State.
Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State.
Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

2009
State-dependent representation independence.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Blame for all.
Proceedings of the Proceedings for the 1st workshop on Script to Program Evolution, 2009

2008
Provenance Traces
CoRR, 2008

Imperative self-adjusting computation.
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Typed closure conversion preserves observational equivalence.
Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!.
Proceedings of the Programming Languages and Systems, 2008

08061 Abstracts Collection -- Types, Logics and Semantics for State.
Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

08061 Executive Summary -- Types, Logics and Semantics for State.
Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

2007
L<sup>3</sup>: A Linear Language with Locations.
Fundam. Informaticae, 2007

Abstract Predicates and Mutable ADTs in Hoare Type Theory.
Proceedings of the Programming Languages and Systems, 2007

2006
Linear Regions Are All You Need.
Proceedings of the Programming Languages and Systems, 2006

Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types.
Proceedings of the Programming Languages and Systems, 2006

2005
A step-indexed model of substructural state.
Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

2003
The logical approach to stack typing.
Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2003

Reasoning about Hierarchical Storage.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

2002
A Stratified Semantics of General References A Stratified Semantics of General References.
Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002


  Loading...