Amal Ahmed


Assistant Professor

College of Computer and Information Science
Northeastern University

Ph.D. (2004) Computer Science
Princeton University

phone: 617.373.2076
fax: 617.373.5121
email: amal at ccs.neu.edu
office: 328 West Village H

address:
Northeastern University
College of Computer and Information Science
328 West Village H
360 Huntington Avenue
Boston, MA 02115


Spring 2014 office hours:
Thursdays, 1:30 - 2:30pm


Research

Programming languages, type systems, semantics, compiler correctness, gradual typing, contracts, language interoperability, state and effects, dependent types, provenance, language-based security, typed intermediate languages, proof-carrying code.


Teaching


Professional Activities


Current Ph.D. Students


Publications

Verifying an Open Compiler Using Multi-Language Semantics.
James T. Perconti and Amal Ahmed.
In Proceedings of the 23rd European Symposium on Programming (ESOP '14), Grenoble, France, April 2014.
Technical report, January 2014.

A Core Calculus for Provenance.
Umut Acar, Amal Ahmed, James Cheney, and Roly Perera.
Journal of Computer Security 21(6): 919-969, 2013.
Special issue devoted to selected papers from POST 2012.

Logical Relations for Fine-Grained Concurrency.
Aaron Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer.
In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '13), Rome, Italy, January 2013.
Technical appendix, July 2012.

A Core Calculus for Provenance.
Umut Acar, Amal Ahmed, James Cheney, and Roly Perera.
In Proceedings of the 1st Conference on Principles of Security and Trust (POST '12), pp. 410-429, Tallinn, Estonia, March 2012.

An Equivalence-Preserving CPS Translation via Multi-Language Semantics.
Amal Ahmed and Matthias Blume.
In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP '11), pp. 431-444, Tokyo, Japan, September 2011.
Technical appendix, April 2011.

Logical Step-Indexed Logical Relations.
Derek Dreyer, Amal Ahmed, and Lars Birkedal.
Logical Methods in Computer Science (LMCS), 7 (2:16), June 2011.
Special issue devoted to selected papers from LICS 2009.
[ This is a significantly revised and expanded version of our LICS 2009 paper. ]

Blame for All.
Amal Ahmed, Robert Bruce Findler, Jeremy Siek, and Philip Wadler.
In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11), pp. 201-214, Austin, Texas, USA, January 2011.

Provenance as Dependency Analysis.
James Cheney, Amal Ahmed, and Umut Acar.
Mathematical Structures in Computer Science (MSCS), 21, pp. 1301-1337, December 2011.
Special Issue on Programming Language Interference and Dependence.

Semantic Foundations for Typed Assembly Languages.
Amal Ahmed, Andrew W. Appel, Christopher Richards, Kedar Swadi, Gang Tan, Daniel Wang.
ACM Transactions on Programming Languages and Systems, 32(3):1-67, March 2010.

Logical Step-Indexed Logical Relations.
Derek Dreyer, Amal Ahmed, and Lars Birkedal.
In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS '09), pp. 71-80, Los Angeles, California, USA, August 2009.

Blame for All.
Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler.
In Proceedings of the 1st International Workshop on Script to Program Evolution (STOP '09), Genova, Italy, July 2009.

State-Dependent Representation Independence.
Amal Ahmed, Derek Dreyer, and Andreas Rossberg.
In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '09), pp. 340-353, Savannah, Georgia, USA, January 2009.
Technical appendix, August 2008.

Typed Closure Conversion Preserves Observational Equivalence.
Amal Ahmed and Matthias Blume.
In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP '08), pp. 157-168, Victoria, British Columbia, Canada, September 2008.
Extended version: Technical Report TR-2008-07, Dept. of Computer Science, University of Chicago, July 2008.

Parametric Polymorphism Through Run-Time Sealing, or, Theorems for Low, Low Prices!
Jacob Matthews and Amal Ahmed.
In Proceedings of the 17th European Symposium on Programming (ESOP '08), pp. 16-31, Budapest, Hungary, March 2008.

Imperative Self-Adjusting Computation.
Umut Acar, Amal Ahmed, and Matthias Blume.
In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '08), pp. 309-322, San Francisco, California, USA, January 2008.
Extended version: Technical Report TR-2007-18, Dept. of Computer Science, University of Chicago, November 2007.

Provenance as Dependency Analysis.
James Cheney, Amal Ahmed, and Umut Acar.
In Proceedings of the 11th International Symposium on Database Programming Languages (DBPL '07), pp. 138-152, Vienna, Austria, September 2007.

L3: A Linear Language with Locations.
Amal Ahmed, Matthew Fluet, and Greg Morrisett.
Fundamenta Informaticae, 77(4):397--449, June 2007.

Abstract Predicates and Mutable ADTs in Hoare Type Theory.
Aleksander Nanevski, Amal Ahmed, Greg Morrisett, and Lars Birkedal.
In Proceedings of the 16th European Symposium on Programming (ESOP '07), pp. 189-204,
Braga, Portugal, March 2007.
Extended version: Harvard University Technical Report TR-14-06, September 2006.

Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types.
Amal Ahmed.
In Proceedings of the 15th European Symposium on Programming (ESOP '06), pp. 69-83, Vienna, Austria, March 2006.
Extended version: Harvard University Technical Report TR-01-06, March 2006.

Linear Regions Are All You Need.
Matthew Fluet, Greg Morrisett, and Amal Ahmed.
In Proceedings of the 15th European Symposium on Programming (ESOP '06), pp. 7-21, Vienna, Austria, March 2006.

A Step-Indexed Model of Substructural State.
Amal Ahmed, Matthew Fluet, and Greg Morrisett.
In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP '05), pp. 78-91, Tallinn, Estonia, September 2005.
Extended version: Harvard University Technical Report TR-16-05, February 2005.

L3: A Linear Language with Locations.
Greg Morrisett, Amal Ahmed, and Matthew Fluet.
In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA '05), Nara, Japan, LNCS 3461, pp. 293-307, Springer-Verlag, April 2005.
[ For more detailed discussion, examples, and proofs, see the technical report below. ]

L3: A Linear Language with Locations.
Amal Ahmed, Matthew Fluet, and Greg Morrisett.
Harvard University Technical Report TR-24-04, July 2004.

Semantics of Types for Mutable State.
Amal Jamil Ahmed.
PhD thesis, Princeton University, 2004.
[ Official version : Double-Spc (246 pp) pdf | ps ] [ Tree-friendly version : Single-Spc (178 pp) pdf | ps ].

An Indexed Model of Impredicative Polymorphism and Mutable References.
Amal Ahmed, Andrew W. Appel, and Roberto Virga.
Draft of January 2003.

Reasoning about Hierarchical Storage.
Amal Ahmed, Limin Jia, and David Walker.
In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS '03), pp. 33-44, Ottawa, Canada, June 2003.

The Logical Approach to Stack Typing.
Amal Ahmed and David Walker.
In Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '03), pp. 74-85, New Orleans, Louisiana, USA, January 2003.

A Stratified Semantics of General References Embeddable in Higher-Order Logic.
Amal Ahmed, Andrew W. Appel, and Roberto Virga.
In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS '02), pp. 75-86, Copenhagen, Denmark, July 2002.

Modeling Collections of Changing Interdependent Objects.
Amal Ahmed, Diane Litman, Anil Mishra, Peter F. Patel-Schneider, and Johannes P. Ros.
In Implementing Application Frameworks: Object-Oriented Frameworks at Work, Mohamed E. Fayad, Douglas C. Schmidt, Ralph Johnson (Editors), John Wiley & Sons, September 1999.