K. Avijit, A. Datta, and R. Harper, Distributed programming with distributed authorization, Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '10, 2010.
DOI : 10.1145/1708016.1708021

M. Backes, C. Hritcu, and M. Maffei, Type-checking zero-knowledge, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, 2008.
DOI : 10.1145/1455770.1455816

J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, Refinement types for secure implementations, CSF, 2008.
DOI : 10.1145/1890028.1890031
URL : https://hal.archives-ouvertes.fr/hal-01294973

Y. Bertot and P. Castéran, Coq'Art: Interactive Theorem Proving and Program Development, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

K. Bhargavan, R. Corin, P. Dénielou, C. Fournet, and J. Leifer, Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, 2009 22nd IEEE Computer Security Foundations Symposium, 2009.
DOI : 10.1109/CSF.2009.26

K. Bhargavan, C. Fournet, and A. D. Gordon, Modular verification of security protocol code by typing, POPL, 2010.

J. Borgstrom, J. Chen, and N. Swamy, Verifying stateful programs with substructural state and hoare types, Proceedings of the 5th ACM workshop on Programming languages meets program verification, PLPV '11, 2011.
DOI : 10.1145/1929529.1929532

I. Cervesato and F. Pfenning, A linear logical framework, Inf. Comput, vol.179, issue.1, 2002.

P. C. Chapin, C. Skalka, and X. S. Wang, Authorization in trust management, ACM Computing Surveys, vol.40, issue.3, 2008.
DOI : 10.1145/1380584.1380587

J. Chen, R. Chugh, and N. Swamy, Type-preserving compilation of end-toend verification of security enforcement, PLDI '10, 2010.

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, 2008.
DOI : 10.1007/978-3-540-78800-3_24

P. Deniélou and N. Yoshida, Dynamic multirole session types, POPL, 2011.

G. Gonthier, A. Mahboubi, E. A. Tassi, A. Gordon, and . Jeffrey, Research Report RR-6455 Authenticity by typing for security protocols, Journal of Computer Security, vol.11, issue.4, pp.451-520, 2003.

A. Guha, M. Fredrikson, B. Livshits, and N. Swamy, Verified Security for Browser Extensions, 2011 IEEE Symposium on Security and Privacy, 2011.
DOI : 10.1109/SP.2011.36

N. Guts, C. Fournet, and F. Z. Nardelli, Reliable Evidence: Auditability by Typing, ESORICS, 2009.
DOI : 10.1016/S0140-3664(02)00049-X

K. Honda, N. Yoshida, and M. Carbone, Multiparty asynchronous session types, POPL, 2008.

L. Jia and S. Zdancewic, Encoding information flow in aura, PLAS, 2009.

L. Jia, J. Vaughan, K. Mazurak, J. Zhao, L. Zarko et al., Aura: A programming language for authorization and audit, ICFP, 2008.

O. Kiselyov, S. P. Jones, and C. Shan, Fun with Type Functions, 2010.
DOI : 10.1007/978-1-84882-912-1_14

S. K. Lahiri, S. Qadeer, and D. Walker, Linear maps. PLPV '11, 2011.

A. Rial and G. Danezis, Privacy-friendly smart metering

P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge et al., Ott: Effective tool support for the working semanticist, JFP, vol.20, issue.1, 2010.

M. Sozeau, Subset Coercions in Coq, TYPES, 2007.
DOI : 10.1007/978-3-540-74464-1_16
URL : https://hal.archives-ouvertes.fr/inria-00628869

N. Swamy, B. J. Corcoran, and M. Hicks, Fable: A Language for Enforcing User-defined Security Policies, 2008 IEEE Symposium on Security and Privacy (sp 2008), 2008.
DOI : 10.1109/SP.2008.29

N. Swamy, J. Chen, and R. Chugh, Enforcing Stateful Authorization and Information Flow Policies in Fine, ESOP, 2010.
DOI : 10.1007/978-3-642-11957-6_28

J. A. Vaughan, L. Jia, K. Mazurak, and S. Zdancewic, Evidence-Based Audit, 2008 21st IEEE Computer Security Foundations Symposium, 2008.
DOI : 10.1109/CSF.2008.24

D. Volpano, G. Smith, and C. Irvine, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2-3, pp.167-187, 1996.
DOI : 10.3233/JCS-1996-42-304