Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Amal Ahmed
[go: Go Back, main page]

Amal Ahmed


Research Assistant Professor
 Toyota Technological Institute at Chicago

Ph.D. (2004) Computer Science
Princeton University

phone: 773.834.6832
fax: 773.834.9881
email: amal at tti-c.org

address:
Toyota Technological Institute at Chicago
6045 S. Kenwood Avenue
Chicago, IL 60637

Research

Programming languages, type systems, semantics, logics, security-preserving compilation, dependent type systems, self-adjusting computation, reasoning about state and effects, language-based security, typed intermediate languages, proof-carrying code.

Teaching

Professional Activities

Publications

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), Savannah, Georgia, USA, January 2009. To appear.
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.