Travelled to:1 × France
1 × Hungary
1 × Italy
1 × Japan
1 × Portugal
1 × United Kingdom
2 × Canada
4 × USA
Collaborated with:M.Blume W.J.Bowman D.Dreyer L.Birkedal U.A.Acar Max S. New Jamie Perconti J.T.Perconti J.Matthews J.Cheney A.Rossberg D.R.Licata Phillip Mates Dustin Jamner R.B.Findler J.G.Siek P.Wadler A.Nanevski G.Morrisett Daniel Patterson 0001 C.Dimoulas Youyou Cong Nick Rioux A.J.Turon J.Thamsborg Olivier Flückiger G.Scherer Ming-Ho Yee Aviral Goel J.Vitek
Talks about:type (6) preserv (3) languag (3) convers (3) closur (3) logic (3) translat (2) parametr (2) gradual (2) equival (2)
Person: Amal Ahmed
DBLP: Ahmed:Amal
Facilitated 1 volumes:
EdContributed to:
20152014
2014
201320112011
200920092008200820082007
201720182018201920192020Wrote 19 papers:
- ICFP-2015-BowmanA #for free
- Noninterference for free (WJB, AA), pp. 101–113.
- ESOP-2014-PercontiA #compilation #multi #semantics #using #verification
- Verifying an Open Compiler Using Multi-language Semantics (JTP, AA), pp. 128–148.
- PPDP-2014-CheneyAA #database #query
- Database Queries that Explain their Work (JC, AA, UAA), pp. 271–282.
- POPL-2013-TuronTABD #concurrent #fine-grained #logic
- Logical relations for fine-grained concurrency (AJT, JT, AA, LB, DD), pp. 343–356.
- ICFP-2011-AhmedB #continuation #multi #semantics
- An equivalence-preserving CPS translation via multi-language semantics (AA, MB), pp. 431–444.
- POPL-2011-AhmedFSW
- Blame for all (AA, RBF, JGS, PW), pp. 201–214.
- LICS-2009-DreyerAB #logic
- Logical Step-Indexed Logical Relations (DD, AA, LB), pp. 71–80.
- POPL-2009-AhmedDR #independence #representation
- State-dependent representation independence (AA, DD, AR), pp. 340–353.
- ESOP-2008-MatthewsA #exclamation #morphism #parametricity #polymorphism #runtime #theorem
- Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices! (JM, AA), pp. 16–31.
- ICFP-2008-AhmedB #equivalence
- Typed closure conversion preserves observational equivalence (AA, MB), pp. 157–168.
- POPL-2008-AcarAB #imperative #self
- Imperative self-adjusting computation (UAA, AA, MB), pp. 309–322.
- ESOP-2007-NanevskiAMB #data type #hoare #type system
- Abstract Predicates and Mutable ADTs in Hoare Type Theory (AN, AA, GM, LB), pp. 189–204.
- PLDI-2017-PattersonPDA #assembly #functional #named
- FunTAL: reasonably mixing a functional language with assembly (DP0, JP, CD, AA), pp. 495–509.
- PLDI-2018-BowmanA #calculus
- Typed closure conversion for the calculus of constructions (WJB, AA), pp. 797–811.
- POPL-2018-BowmanCRA #continuation
- Type-preserving CPS translation of Σ and Π types is not not possible (WJB, YC, NR, AA), p. 33.
- POPL-2018-FluckigerSYGAV #correctness #optimisation
- Correctness of speculative optimizations with dynamic deoptimization (OF, GS, MHY, AG, AA, JV), p. 28.
- POPL-2019-NewLA #type system
- Gradual type theory (MSN, DRL, AA), p. 31.
- PPDP-2019-MatesPA
- Under Control: Compositionally Correct Closure Conversion with Mutable State (PM, JP, AA), p. 15.
- POPL-2020-NewJA #parametricity
- Graduality and parametricity: together again for the first time (MSN, DJ, AA), p. 32.