Dependent Types and Program Equivalence.
Limin Jia, Jianzhou Zhao, Vilhelm Sjoberg and Stephanie Weirich.
In Proceedings of 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), to appear, January 2010.

Formally Verifiable Networking.
Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwish Basu.
In 8th Workshop on Hot Topics in Networks (ACM SIGCOMM HotNets-VIII) , October 2009. [PDF]

Language Support for Processing Distributed Ad Hoc Data.
Kenny Q. Zhu, Daniel S. Dantas, Kathleen Fisher, Limin Jia, Yitzhak Mandelbaum, Vivek Pai and David Walker.
In Proceedings of ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP) , September 2009. [PDF]
Long version appeared as Princeton Univ. Technical Report TR-826-08, July 2008. [PDF]

Encoding Information Flow in AURA.
Limin Jia and Steve Zdancewic.
In Proceedings of ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS 2009), June 2009. [PDF]
Long version appeared as Univ. of Pennsylvania Technical Report MS-CIS-09-08, July 2008. [PDF]

xDomain: Cross-border proofs of access.
Lujo Bauer, Limin Jia, Michael K. Reiter, and David Swasey.
In Proceedings of the 14th ACM Symposium on Access Control Models and Technologies, June 2009. [PDF]
Long version appeared as Carnegie Mellow University Technical Report CMU-CyLab-09-005. [PDF]

AURA: A programming language for authorization and audit.
Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr and Steve Zdancewic.
In Proceedings of the 2008 SIGPLAN International Conference on Functional Programming (ICFP), September 2008. [PDF]
Long version appeared as Univ. of Pennsylvania Technical Report MS-CIS-08-10, July 2008. [PDF]

Evidence-based Audit.
Jeffrey A. Vaughan, Limin Jia, Karl Mazurak and Steve Zdancewic.
In Proceedings of 21st IEEE Computer Security Foundations Symposium (CSF), June 2008. [PDF]
Long version appeared as Univ. of Pennsylvania Technical Report MS-CIS-08-09, April 2008. [PDF]

Expressing Heap-shape Contracts in Linear Logic.
Frances Perry, Limin Jia and David Walker.
In Proceedings of the 5th International Conference on Generative Programming and Component Engineering (GPCE), October 2006. [PDF]
An earlier version appeared in the Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE), January 2006. [PDF]

ILC: A Foundation for Automated Reasoning About Pointer Programs.
Limin Jia and David Walker.
In Programming Languages and Systems: 15th European Symposium on Programming, ESOP 2006, Lecture Notes in Computer Science 3924, March 2006. [PDF]
Super short version appeared in 20th IEEE Symposium on Logic in Computer Science (LICS), short paper, June 2005. [PDF]
Long version appeared as Princeton University Technical Report TR-738-05, October 2005. [PDF]

Certifying Compilation for a Language with Stack Allocation.
Limin Jia, Frances Spalding, David Walker and Neal Glew.
In Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS), June 2005. [PDF]
Long version appeared as Princeton University Technical Report TR-724-05, March 2005. [PDF]

Reasoning About Hierarchical Storage.
Amal Ahmed, Limin Jia and David Walker.
In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS), June 2003. [PDF]

Linear Logic, Heap-shape Patterns and Imperative Programming.
Limin Jia and David Walker. [PDF]
Long version appeared as Princeton University Technical Report TR-762-06, July 2006. [PDF]