EN FR
EN FR




Bibliography

Major publications by the team in recent years
  • 1G. Barthe, C. Fournet (editors)

    Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, Lecture Notes in Computer Science, Springer, 2008, vol. 4912.
  • 220th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy, IEEE Computer Society, 2007.
  • 3Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, 2009, IEEE Computer Society, 2009.
  • 4P. Ning, P. F. Syverson, S. Jha (editors)

    Proceedings of the 2008 ACM Conference on Computer and Communications Security, CCS 2008, Alexandria, Virginia, USA, October 27-31, 2008, ACM, 2008.
  • 5F. Besson, T. Blanc, C. Fournet, A. D. Gordon.

    From Stack Inspction to Access Control: A Security Analysis for Libraries, in: 17th IEEE Computer Security Foundations Workshop, June 2004, p. 61–75.
  • 6K. Bhargavan, R. Corin, P.-M. Deniélou, C. Fournet, J. J. Leifer.

    Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, in: CSF, IEEE Computer Society, 2009, p. 124-140.
  • 7R. Corin, P.-M. Deniélou, C. Fournet, K. Bhargavan, J. J. Leifer.

    Secure Implementations for Typed Session Abstractions, in: 20th IEEE Computer Security Foundations Symposium (CSF'07), Venice, Italy, IEEE, July 2007, p. 170–186.

    http://www.msr-inria.inria.fr/projects/sec/sessions/
  • 8R. Corin, P.-M. Deniélou.

    A Protocol Compiler for Secure Sessions in ML, in: TGC, G. Barthe, C. Fournet (editors), Lecture Notes in Computer Science, Springer, 2007, vol. 4912, p. 276-293.
  • 9R. Corin, P.-M. Deniélou, C. Fournet, K. Bhargavan, J. J. Leifer.

    Secure Implementations for Typed Session Abstractions, in: CSF, IEEE Computer Society, 2007, p. 170-186.
  • 10R. Corin, P.-M. Deniélou, C. Fournet, K. Bhargavan, J. J. Leifer.

    A secure compiler for session abstractions, in: Journal of Computer Security, 2008, vol. 16, no 5, p. 573-636.
  • 11C. Fournet, G. Gonthier.

    The Reflexive Chemical Abstract Machine and the Join-Calculus, in: Proceedings of the 23rd Annual Symposium on Principles of Programming Languages (POPL), (St. Petersburg Beach, Florida), ACM, January 1996, p. 372–385.
  • 12C. Fournet, G. Gonthier, J.-J. Lévy, L. Maranget, D. Rémy.

    A Calculus of Mobile Agents, in: CONCUR '96: Concurrency Theory (7th International Conference), Pisa, Italy, U. Montanari, V. Sassone (editors), LNCS, Springer, August 1996, vol. 1119, p. 406–421.
  • 13C. Fournet, C. Laneve, L. Maranget, D. Rémy.

    Inheritance in the join calculus, in: Journal of Logics and Algebraic Programming, September 2003, vol. 57, no 1–2, p. 23–29.
  • 14A. Hobor, A. Appel, F. Zappa Nardelli.

    Oracle Semantics for Concurrent Separation Logic, in: 17th European Symposium on Programming (ESOP'08), April 2007.
  • 15J. J. Leifer, G. Peskine, P. Sewell, K. Wansbrough.

    Global abstraction-safe marshalling with hash types, in: Proc. 8th ICFP, 2003, Extended Abstract of INRIA Research Report 4851.

    http://hal.inria.fr/inria-00071732/fr/
  • 16M. Merro, F. Zappa Nardelli.

    Behavioural theory for Mobile Ambients, in: Journal of ACM, November 2005, vol. 52, no 6, p. 961–1023.
  • 17M. Qin, L. Maranget.

    Expressive Synchronization Types for Inheritance in the Join Calculus, in: Proceedings of APLAS'03, Beijing China, LNCS, Springer, November 2003.
  • 18S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Ridge, T. Braibant, M. O. Myreen, J. Alglave.

    The semantics of x86-CC multiprocessor machine code, in: POPL, 2009, p. 379-391.
Publications of the year

Doctoral Dissertations and Habilitation Theses

  • 19N. Guts.

    Auditability for security protocols, Université Denis Diderot Paris 7, 2011.

Articles in International Peer-Reviewed Journal

Articles in National Peer-Reviewed Journal

International Conferences with Proceedings

  • 22M. Batty, K. Memarian, S. Owens, S. Sarkar, P. Sewell.

    Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER, in: Proc. POPL 2012, 2011, to appear.
  • 23K. Bhargavan, Q. Lefebvre.

    Verified Android Cryptographic Applications, in: 5th International Workshop on Analysis of Security APIs (ASA-5), July 2011.
  • 24C. Fournet, K. Bhargavan, A. D. Gordon.

    Cryptographic Verification by Typing for a Sample Protocol Implementation, in: Foundations of Security Analysis and Design VI (FOSAD'10), 2011, p. 66-100.
  • 25S. Owens, P. Böhm, F. Zappa Nardelli, P. Sewell.

    Lem: A Lightweight Tool for Heavyweight Semantics, in: ITP, 2011.

    http://www.cl.cam.ac.uk/~so294/documents/itp11.pdf
  • 26S. Sarkar, P. Sewell, J. Alglave, L. Maranget, D. Williams.

    Understanding POWER Multiprocessors, in: Proceedings of 32nd ACMSIGPLAN Conference on Programming Language Design and Implementation, June 2011, p. 175–186.

    http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf
  • 27N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, J. Yang.

    Secure Distributed Programming with Value-dependent Types, in: 16th ACM SIGPLAN International Conference on Functional Programming, Tokyo, Japan, 2011, p. 266-278, Related Projects * F*: A Verifying ML Compiler for Distributed Programming.

    http://hal.inria.fr/inria-00596715/en
  • 28V. Vafeiadis, F. Zappa Nardelli.

    Verifying Fence Elimination Optimisations, in: in Proc. SAS 2011, 2011.

    http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/fenceelim.pdf
  • 29J. Ševčík, V. Vafeiadis, F. Zappa Nardelli, P. Sewell, S. Jagannathan.

    Relaxed-Memory Concurrency and Verified Compilation, in: Proc. POPL, 2011.

    http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/paper.pdf

Scientific Books (or Scientific Book chapters)

  • 30J. Alglave, L. Maranget.

    Stability in Weak Memory Models, in: Computer Aided Verification, G. Gopalakrishnan, S. Qadeer (editors), Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 2011, vol. 6806, p. 50–66.

    http://dx.doi.org/10.1007/978-3-642-22110-1_6
  • 31J. Alglave, L. Maranget, S. Sarkar, P. Sewell.

    Litmus Running Tests against Hardware, in: Tools and Algorithms for the Construction and Analysis of Systems, P. Abdulla, K. Leino (editors), Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 2011, vol. 6605, p. 41-44.

Other Publications

References in notes
  • 36R. Milner.

    Communication and Concurrency, International Series on Computer Science, Prentice Hall, 1989.
  • 37R. Milner, J. Parrow, D. Walker.

    A Calculus of Mobile Processes, Parts I and II, in: Journal of Information and Computation, September 1992, vol. 100, p. 1–77.
  • 38B. C. Pierce.

    Types and Programming Languages, The MIT Press, 2002.