Research Interests

• The Cryptyc Project: foundations of computer security; type systems for secrecy and authenticity.

• The Temporal Aspects Project: formal basis of aspect-oriented programming; aspects for security.

• The Full Abstraction Factory: mathematical foundations of programming languages; scalable models of object-based component systems.

Recent Publications

• Lambda RBAC: Programming with Role-Based Access Control. R. Jagadeesan, A. S. A. Jeffrey, C. Pitcher and J. Riely. In Logical Methods In Computer Science. 2008. To appear. Available on-line.

• Efficient and Expressive Tree Filters. M. Benedikt and A. S. A. Jeffrey. In Proc. Foundations of Software Technology and Theoretical Computer Science. Springer-Verlag. 2007. To appear. Available on-line.

• Full Abstraction for Polymorphic Pi-Calculus. A. S. A. Jeffrey and J. Rathke. In Theoretical Computer Science. 2007. To appear. Available on-line.

• Pattern-Matching Spi-Calculus. C. Haack and A. S. A. Jeffrey. In Information and Computation. 204 (8). 2006. pp. 1195-1263. Available on-line.

• Typed Parametric Polymorphism for Aspects. R. Jagadeesan, A. S. A. Jeffrey and J. Riely. In Science of Computer Programming. 63 (3). 2006. pp. 267--296. Available on-line.

• Dynamic Model Checking of C Cryptographic Protocol Implementations. A. S. A. Jeffrey and R. Ley-Wild. In Proc. Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis. 2006. Available on-line.

• Lambda-RBAC: Programming with Role-Based Access Control. In Proc. Int. Colloq. Automata, Languages and Programming. Springer-Verlag. 2006. pp. 456-467. Available on-line.

• A Fully Abstract May Testing Semantics for Concurrent Objects. A. S. A. Jeffrey and J. Rathke. In Theoretical Computer Science. vol. 338. 2005. pp. 17-63. Available on-line.

• Contextual Equivalence for Higher-Order Pi-Calculus Revisited. A. S. A. Jeffrey and J. Rathke. In Logical Methods in Computer Science. 1 (1:4). 2005. pp. 1-22. Available on-line.

• Full Abstraction for Polymorphic Pi-Calculus. A. S. A. Jeffrey and J. Rathke. In Proc. Foundations of Software Science and Computation Structures. Springer-Verlag. 2005. pp. 266-281. Full version to appear in Theoretical Computer Science. Available on-line.

• Java Jr.: Fully Abstract Trace Semantics for a Core Java Language. A. S. A. Jeffrey and J. Rathke. In Proc. European Symposium on Programming. Springer-Verlag. 2005. pp. 423-438. Available on-line.

• Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus. A. D. Gordon and A. S. A. Jeffrey. In Proc. Concur. Springer-Verlag. 2005. pp. 186-201. Available on-line.

• Timed Spi-calculus with Types for Secrecy and Authenticity. In Proc. Concur. Springer-Verlag. 2005. pp. 202-216. Available on-line.

Co-authors

• Luca Aceto, Department of Computer Science, Aalborg University.

• Michael Benedikt, Computing Laboratory, Oxford University.

• Glenn Bruns, Bell Labs, Lucent Technologies.

• Andrew D. Gordon, Microsoft Research.

• Christian Haack, Security of Systems Group, University of Nijmegen.

• Matthew Hennessy, Informatics, University of Sussex.

• Radha Jagadeesan, CTI, DePaul University.

• Corin Pitcher, CTI, DePaul University.

• Ruy Ley-Wild, School of Computer Science, Carnegie Mellon University.

• Julian Rathke, Informatics, University of Sussex.

• James Riely, CTI, DePaul University.

• Ralf Schweimeier, Department of Computing, City University.

• Ian Wakeman, Informatics, University of Sussex.