The papers given here are not necessarily identical to any previously published paper. Copyright and all rights therein are maintained by the authors or by other copyright holders. Additional bibliographic details appear in these bibtex and pdf files. Please contact me if you don't find the paper you are looking for.

Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
(.pdf), with
Pierre-Yves Strub, Nikhil Swamy, and Juan Chen, in *ACM Symposium on Principles of Programming Languages (POPL'12)*, pages 571--583.
January 2012.
© ACM.

Information-Flow Types for Homomorphic Encryptions
(.pdf), with
Jérémy Planul and Tamara Rezk, in *18th ACM Conference on Computer and Communications Security (CCS'11)*, pages 351--360.
October 2011.
© ACM.

Modular Code-Based Cryptographic Verification
(.pdf), with
Markulf Kohlweiss and Pierre-Yves Strub, in *18th ACM Conference on Computer and Communications Security (CCS'11)*, pages 341--350.
October 2011.
© ACM.

Secure Distributed Programming with Value-Dependent Types
(.pdf), with
Nikhil Swamy, Juan Chen, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang, in *ICFP*.
September 2011.
See also the full paper at MSR-TR-2011-37.

Compiling Information-Flow Security to Minimal Trusted Computing Bases
(.pdf),
with Jérémy Planul, in *Programming Languages and Systems (ESOP'11)*, *LNCS* 6602, pages 216--235.
March 2011.
© Springer-Verlag.

**Typechecking Higher-Order Security Libraries**, with
Karthikeyan Bhargavan and Nataliya Guts, in *APLAS*, pages 47--62.
2010.

Modular Verification of Security Protocol Code by Typing
(.pdf), with
K. Bhargavan and A. D. Gordon, in *ACM Symposium on Principles of Programming Languages (POPL'10)*, pages 445--456.
January 2010.
© ACM.

A Security-Preserving Compiler for Distributed Programs: From Information-Flow Policies to Cryptographic Mechanisms
(.pdf), with
Gurvan le Guernic and Tamara Rezk, in *ACM Conference on Computer and Communications Security (CCS'09)*, pages 432--441.
November 2009.
© ACM.

Reliable Evidence: Auditability by Typing
(.pdf), with
Nataliya Guts and Francesco Zappa Nardelli, in *14th European Symposium on Research in Computer Security (ESORICS 2009)*, *LNCS* 5789, pages 168--183.
September 2009.
© Springer-Verlag.

Secure Enforcement for Global Process Specifications
(.pdf), with
Jérémy Planul and Ricardo Corin, in *20th International Conference on Concurrency Theory (CONCUR'09)*, *LNCS* 5710, pages 511--526.
September 2009.
© Springer-Verlag.

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions
(.pdf), with
Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, and James J. Leifer, in *22nd IEEE Computer Security Foundations Symposium (CSF'09)*, pages 124--140.
July 2009.
© IEEE.

**High-Level Programming for E-Cash (Extended Abstract)**, with
Nataliya Guts and Francesco Zappa Nardelli, in *1st Computational and Symbolic Proofs of Security Workshop*.
2009.

Cryptographically Verified Implementations for TLS
(.pdf), with
Karthikeyan Bhargavan, Ricardo Corin, and Eugen Zalinescu, in *ACM Conference on Computer and Communications Security (CCS'08)*, pages 459--468.
October 2008.
© ACM.

Code-Carrying Authorization
(.pdf), with
Sergio Maffeis, Martín Abadi, and Andrew D. Gordon, in *13th European Symposium on Research in Computer Security (ESORICS'08)*, *LNCS* 5283, pages 563-579.
October 2008.
© Springer-Verlag.

Refinement Types for Secure Implementations
(.pdf), with
Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, in *21st IEEE Computer Security Foundations Symposium (CSF'08)*, pages 17--32.
June 2008.
© IEEE.

A Formal Implementation of Value Commitment
(.pdf), with
Nataliya Guts and Francesco Zappa Nardelli, in *Programming Languages and Systems (ESOP'08)*, *LNCS* 4960, pages 383--397.
March 2008.
© Springer-Verlag.

Verified Implementations of the Information Card Federated Identity-Management Protocol
(.pdf), with
Karthikeyan Bhargavan, Andrew D. Gordon, and Nikhil Swamy, in *Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS'08)*, pages 123--135.
March 2008.
© ACM.

Cryptographically Sound Implementations for Typed Information-Flow Security
(.pdf),
with Tamara Rezk, in *35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08)*, pages 323--335.
January 2008.
© ACM.

Secure Implementations of Typed Session Abstractions
(.pdf), with
Ricardo Corin, Pierre-Malo Deniélou, Karthikeyan Bhargavan, and James J. Leifer, in *20th IEEE Computer Security Foundations Symposium (CSF20)*, pages 170--186.
July 2007.
© IEEE.

Design and Semantics of a Decentralized Authorization Language
(.pdf), with
Moritz Y. Becker and Andrew D. Gordon, in *20th IEEE Computer Security Foundations Symposium (CSF20)*, pages 3--15.
July 2007.
© IEEE.

A Type Discipline for Authorization in Distributed Systems
(.pdf), with
Andrew D. Gordon and Sergio Maffeis, in *20th IEEE Computer Security Foundations Symposium (CSF20)*, pages 31--45.
July 2007.
© IEEE.

Computational Secrecy by Typing for the Pi Calculus
(.pdf), with
Martín Abadi and Ricardo Corin, in *Programming Languages and Systems 4th Asian Symposium (APLAS 2006)*, *LNCS* 4279, pages 253--269.
November 2006.
© Springer-Verlag.

Verified Reference Implementations of WS-Security Protocols
(.pdf), with
Karthikeyan Bhargavan and Andrew D. Gordon, in *Web Services and Formal Methods, Third International Workshop (WS-FM 2006)*, *LNCS* 4184, pages 88--106.
September 2006.
© Springer-Verlag.

Cryptographically Sound Implementations for Communicating Processes (Extended Abstract)
(.pdf),
with Pedro Adao, in *33rd International Colloquium on Automata, Languages and Programming (ICALP 2006)*, *LNCS* 4052, pages 83--94.
July 9--16 2006.
© Springer-Verlag.

Verified Interoperable Implementations of Security Protocols
(.pdf), with
Karthikeyan Bhargavan, Andrew D. Gordon, and Stephen Tse, in *19th IEEE Computer Security Foundations Workshop (CSFW'06)*, pages 139--152.
June 2006.
© IEEE.

An Advisor for Web Services Security Policies
(.pdf), with
Karthikeyan Bhargavan, Andrew D. Gordon, and Greg O'Shea, in *SWS'05: Proceedings of the 2005 ACM Workshop on Secure Web Service*, pages 1--9.
October 2005.
© ACM.

Automated Verification of Selected Equivalences for Security Protocols
(.pdf), with
Bruno Blanchet and Martín Abadi, in *20th IEEE Symposium on Logic in Computer Science (LICS 2005)*, pages 331--340.
June 2005.
The full version now appears in Journal of Logic and Algebraic Programming.
© IEEE.

A Type Discipline for Authorization Policies
(.pdf), with
Andrew D. Gordon and Sergio Maffeis, in *Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005*, *LNCS* 3444, pages 141--156.
April 2005.
© Springer-Verlag.

Secure Sessions for Web Services
(.pdf), with
Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, in *SWS'04: Proceedings of the 2004 Workshop on Secure Web Services*, pages 56--66.
October 2004.
© ACM.

Verifying Policy-Based Security for Web Services
(.pdf), with
K. Bhargavan and A. D. Gordon, in *11th ACM Conference on Computer and Communications Security (CCS'04)*, pages 268-277.
October 2004.
© ACM.

Ethernet Topology Discovery without Network Assistance
(.pdf), with
Richard Black and Austin Donnelly, in *Proceedings of the 12th IEEE International Conference on Network Protocols (ICNP 2004)*, pages 328--339.
October 2004.
© IEEE.

Stuck-Free Conformance
(.ps), with
C. A. R. Hoare, Sriram K. Rajamani, and Jakob Rehof, in *Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)*, *LNCS* 3114, pages 242--254.
July 2004.
© Springer-Verlag.

TulaFale: A Security Tool for Web Services
(.pdf), with
K. Bhargavan, A. D. Gordon, and R. Pucella, in *International Symposium on Formal Methods for Components and Objects (FMCO'03)*, *LNCS* 3188, pages 197--222.
2004.
© Springer-Verlag.

From Stack Inspection to Access Control: A Security Analysis for Libraries
(.ps), with
Frédéric Besson, Tomasz Blanc, and Andrew D. Gordon, in *17th IEEE Computer Security Foundations Workshop (CSFW'04)*, pages 61--75.
June 2004.
© IEEE.

Just Fast Keying in the Pi Calculus
(.pdf), with
Martín Abadi and Bruno Blanchet, in *Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004*, *LNCS* 2986, pages 340--354.
March 2004.
© Springer-Verlag.

A Semantics for Web Services Authentication
(.pdf), with
K. Bhargavan and A. D. Gordon, in *31st ACM Symposium on Principles of Programming Languages (POPL'04)*, pages 198--209.
January 2004.
An extended version appears as Microsoft Research Technical Report MSR-TR-2003-83.
© ACM.

Access Control based on Execution History
(.pdf)
(.ps),
with Martín Abadi, in *Network and Distributed System Security Symposium (NDSS'03)*, pages 107--121.
February 2003.
© Internet Society.

Hiding Names: Private Authentication in the Applied Pi Calculus
(.pdf)
(.ps),
with Martín Abadi, in *Software Security -- Theories and Systems. Mext-NSF-JSPS International Symposium, Tokyo, November 2002 (ISSS'02)*, *LNCS* 2609, pages 317--338.
2003.
© Springer-Verlag.

Stack Inspection: Theory and Variants
(.pdf)
(.ps),
with Andrew D. Gordon, in *Conference record of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'02)*, pages 307--318.
January 2002.
© ACM.

Modern Concurrency Abstractions for C#
(.pdf)
(.ps), with
Nick Benton and Luca Cardelli, in *ECOOP 2002 -- Object Oriented Programming*, *LNCS* 2374, pages 415--440.
June 2002.
© Springer-Verlag.

Mobile values, new names, and secure communication
(.pdf)
(.ps),
with Martín Abadi, in *28th ACM Symposium on Principles of Programming Languages (POPL'01)*, pages 104--115.
2001.
© ACM.

Authentication Primitives and their Compilation
(.pdf)
(.ps), with
Martín Abadi and Georges Gonthier, in *Conference record of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00)*, pages 302--315.
January 2000.
© ACM.

An Asynchronous, Distributed Implementation of Mobile Ambients
(.pdf)
(.ps), with
Jean-Jacques Lévy and Alan Schmitt, in *Proceedings of IFIP TCS 2000*, *LNCS* 1872, pages 348--364.
17--19 August 2000.
© Springer-Verlag.

Inheritance in the join-calculus (Extended Abstract)
(.pdf)
(.ps), with
Cosimo Laneve, Luc Maranget, and Didier Rémy, in *FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science*, *LNCS* 1974, pages 397--408.
December 2000.
The full version now appears in Journal of Logic and Algebraic Programming.
© Springer-Verlag.

A Top-Down Look at a Secure Message
(.ps), with
Martín Abadi and Georges Gonthier, in *Proceedings of the Nineteenth Conference on the Foundations of Software Technology and Theoretical Computer Science (FST&TCS '99)*, *LNCS* 1738, pages 122--141.
December 1999.
© Springer-Verlag.

Secure Communications Processing for Distributed Languages
(.pdf)
(.ps), with
Martín Abadi and Georges Gonthier, in *Proceedings of the 1999 IEEE Symposium on Security and Privacy*, pages 74--88.
May 1999.
© IEEE.

**An Implementation of Ambients in JoCaml**,
with Alan Schmitt, in *5th Mobile Object Systems Workshop: Programming Languages for Wide-Area Networks*.
June 1999.

Secure Implementation of Channel Abstractions
(.ps), with
Martín Abadi and Georges Gonthier, in *Proceedings of LICS '98*, pages 105--116.
June 1998.
© IEEE.

Bisimulations in the Join-Calculus
(.ps), with
Michele Boreale and Cosimo Laneve, in *Programming Concepts and Methods, IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET '98)*.
June 1998.
© Chapman and Hall.

A Hierarchy of Equivalences for Asynchronous Calculi (extended abstract)
(.ps),
with Georges Gonthier, in *Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP '98)*, *LNCS* 1443, pages 844-855.
July 1998.
© Springer-Verlag.

Implicit Typing à la ML for the join-calculus
(.ps), with
Cosimo Laneve, Luc Maranget, and Didier Rémy, in *Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97)*, *LNCS* 1243, pages 196--212.
1--4 July 1997.
© Springer-Verlag.

A Calculus of Mobile Agents
(.ps), with
Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, and Didier Rémy, in *Proceedings of the 7th International Conference on Concurrency Theory (CONCUR '96)*, *LNCS* 1119, pages 406--421.
26--29 August 1996.
© Springer-Verlag.

The Reflexive Chemical Abstract Machine and the Join-Calculus
(.ps),
with Georges Gonthier, in *Conference record of the 23th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'96)*, pages 372--385.
January 1996.
© ACM.

Cryptographic Verification by Typing for a Sample Protocol Implementation
(.pdf), with
Karthik Bhargavan and Andrew D. Gordon, in *Proceedings of the Foundations of Seccurity and Design VI Summer School (FOSAD 2010)*, *LNCS*.
September 2011.
© IOS Press.
© Springer-Verlag.

**Principles and Applications of Refinement Types**,
with Andrew D. Gordon, in *International Summer School Logics and Languages for Reliability and Security, Marktoberdorf, August 2009*.
October 2010.
Also Technical Report MSR-TR-2009-147.
© IOS Press.

JoCaml: a Language for Concurrent Distributed and Mobile Programming
(.pdf), with
Fabrice Le Fessant, Luc Maranget, and Alan Schmitt, in *Advanced Functional Programming, 4th International School, Oxford, August 2002*, *LNCS* 2638, pages 129--158.
2003.
© Springer-Verlag.

The Join Calculus: a Language for Distributed Mobile Programming
(.pdf)
(.ps),
with Georges Gonthier, in *Applied Semantics. International Summer School, APPSEM 2000, Caminha, Portugal, September 2000*, *LNCS* 2395, pages 268--332.
August 2002.
© Springer-Verlag.

**Refinement Types for Secure Implementations**, with
Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, *ACM Transactions on Programming Languages and Systems*.
2010.
To appear. An short version appears in CSF'08. See also Microsoft Research Technical Report MSR-TR-2008-118 SP1.
© ACM.

**SecPAL: Design and Semantics of a Decentralized Authorization Language**, with
Moritz Y. Becker and Andrew D. Gordon, *Journal of Computer Security (Special issue for CSF'07)*.
2009.
To appear.
© IOS Press.

**A Secure Compiler for Session Abstractions**, with
Ricardo Corin, Pierre-Malo Deniélou, Karthikeyan Bhargavan, and James J. Leifer, *Journal of Computer Security (Special issue for CSF'07)* 16(5):573--636.
2008.
© IOS Press.

Automated Verification of Selected Equivalences for Security Protocols
(.pdf), with
Bruno Blanchet and Martín Abadi, *Journal of Logic and Algebraic Programming* 75(1):3--51.
2008.
A short version appears in LICS'05.
© Elsevier.

**Verified Interoperable Implementations of Security Protocols**, with
Karthikeyan Bhargavan, Andrew D. Gordon, and Stephen Tse, *ACM Transactions on Programming Languages and Systems* 31(1):1--61.
December 2008.
© ACM.

**Verifying Policy-Based Web Services Security**, with
Karthikeyan Bhargavan and Andrew D. Gordon, *ACM Transactions on Programming Languages and Systems* 30(6).
October 2008.
© ACM.

**Just Fast Keying in the Pi Calculus**, with
Martín Abadi and Bruno Blanchet, *ACM Transactions on Information and System Security (TISSEC)* 10(3).
July 2007.
An extended abstract appears in Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004.
© ACM.

**A Type Discipline for Authorization Policies**, with
A. D. Gordon and S. Maffeis, *ACM Transactions on Programming Languages and Systems* 29(5).
August 2007.
© ACM.

Secure Sessions for Web Services
(.pdf), with
Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, *ACM Transactions on Information and System Security (TISSEC)* 10(2).
May 2007.
© ACM.

A Hierarchy of Equivalences for Asynchronous Calculi
(.pdf)
(.ps),
with Georges Gonthier, *Journal of Logic and Algebraic Programming* 63(1):131--173.
April 2005.
An extended abstract appears in ICALP'98.
© Elsevier.

**A Semantics for Web Services Authentication**, with
Karthikeyan Bhargavan and Andrew D. Gordon, *Theoretical Computer Science* 340(1):102--153.
June 2005.
See also Microsoft Research Technical Report MSR-TR-2003-83.
© Elsevier.

Private Authentication
(.pdf),
with Martín Abadi, *Theoretical Computer Science* 322(3):427--476.
September 2004.
Special issue on Foundations of Wide Area Network Computing. Parts of this work were presented at PET'02 (LNCS 2482) and ISSS'02 (LNCS 2602).
© Elsevier.

Modern Concurrency Abstractions for C#
(.pdf), with
Nick Benton and Luca Cardelli, *ACM Transactions on Programming Languages and Systems* 26(5):769--804.
September 2004.
An extended abstract appears in ECOOP'02 (LNCS 2374).
© ACM.

Stack Inspection: Theory and Variants
(.pdf),
with Andrew D. Gordon, *ACM Transactions on Programming Languages and Systems* 25(3):360--399.
2003.
An extended abstract appears in POPL'02.
© ACM.

**Inheritance in the join calculus**, with
Cosimo Laneve, Luc Maranget, and Didier Rémy, *Journal of Logic and Algebraic Programming* 57(1--2):23--69.
September 2003.
© Elsevier.

**Secure Implementation of Channel Abstractions**, with
Martín Abadi and Georges Gonthier, *Information and Computation* 174(1):37--83.
April 2002.
© Elsevier.

Bisimulations in the Join-Calculus
(.pdf)
(.ps),
with Cosimo Laneve, *Theoretical Computer Science* 266(1-2):569--603.
September 2001.
© Elsevier.

Pre- and Post-Conditions for Security Typechecking
(.pdf), with
Karthikeyan Bhargavan and Nataliya Guts, in *Workshop on Foundations of Security and Privacy (FCS-PrivMod 2010)*.
July 2010.

Refinement Types for Secure Implementations (.pdf), with Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, Microsoft Research Technical Report (MSR-TR-2008-118). 2008. Revised: 2010.

**Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers**,
with Gilles Barthe, *LNCS* 4912.
2008.
© Springer-Verlag.

**A Secure Compiler for Session Abstractions**, with
Ricardo Corin, Pierre-Malo Deniélou, Karthikeyan Bhargavan, and James Leifer, MSR-INRIA Joint Centre .
2008.
Prototype implementation available at \urlhttp://msr-inria.inria.fr/projects/sec/sessions.

**A Computational Verifier for Protocol Code (fs2cv)**, with
Karthikeyan Bhargavan, Ricardo Corin, and Eugen Zalinescu, MSR-INRIA Joint Centre .
2008.
Prototype implementation available at \urlhttp://msr-inria.inria.fr/projects/sec/fs2cv.

**Crypto-Verifying Protocol Implementations in ML**, with
Karthikeyan Bhargavan and Ricardo Corin, in *Proceedings of the 3rd Workshop on Formal and Computational Cryptography (FCC'07)*.
July 2007.

SecPAL: Design and Semantics of a Decentralized Authorization Language (.pdf), with Moritz Y. Becker and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2006-120). September 2006.

**A Type Discipline for Authorization Policies**, with
A. D. Gordon and S. Maffeis, Microsoft Research (MSR-TR-2005-01).
2005.

Stuck-Free Conformance (.ps), with C. A. R. Hoare, Sriram K. Rajamani, and Jakob Rehof, Microsoft Research Technical Report (MSR-TR-2004-69). July 2004.

A Semantics for Web Services Authentication (.pdf), with Karthikeyan Bhargavan and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2003-83). February 2004.

**Secure Sessions for Web Services**, with
Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2004-114).
2004.

A Distributed Implementation of Ambients (.ps), with Jean-Jacques Lévy and Alan Schmitt. 2000. Manuscript, subsumes papers presented at MOS'99 and FST-TCS 2000.

Secure implementation of channel abstractions (.ps), with Martín Abadi and Georges Gonthier. September 2000. Manuscript, subsumes papers presented at LICS'98 and S&P'99.

**Weak Bisimulations by Decreasing Diagrams**,
with Georges Gonthier.
March 1999.
Draft.

**An Implementation of Ambients in JoCAML**,
with Alan Schmitt.
1999.
Software available from http://join.inria.fr/ambients.html.

**The Join-Calculus language (version 1.03)**,
with Luc Maranget.
June 1997.
Source distribution and documentation available from http://join.inria.fr/.

The Join-Calculus: a Calculus for Distributed Mobile Programming (.ps.gz) (.pdf). November 1998. Ecole Polytechnique, Palaiseau. Also published by INRIA, TU-0556.