L 3 : A linear language with locations, Fundamenta Informaticae, vol.77, issue.4, pp.397-449, 2007. ,
Typestate-oriented programming, Proceeding of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications, OOPSLA '09, pp.1015-1022, 2009. ,
DOI : 10.1145/1639950.1640073
The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS), pp.49-69, 2004. ,
DOI : 10.1007/978-3-540-30569-9_3
Smallfoot: Modular Automatic Assertion Checking with Separation Logic, Formal Methods for Components and Objects, pp.115-137, 2005. ,
DOI : 10.1007/11804192_6
Modular typestate checking of aliased objects, Object-Oriented Programming, Systems, Languages , and Applications (OOPSLA), pp.301-320, 2007. ,
Practical API Protocol Checking with Access Permissions, European Conference on Object-Oriented Programming, pp.195-219, 2009. ,
DOI : 10.1109/TSE.1986.6312929
Semantics of fractional permissions with nesting, ACM Transactions on Programming Languages and Systems, vol.32, issue.6, 2010. ,
Step-Indexed Kripke Model of Separation Logic for Storable Locks, Electronic Notes in Theoretical Computer Science, vol.276, pp.121-143, 2011. ,
DOI : 10.1016/j.entcs.2011.09.018
Characteristic Formulae for Mechanized Program Verification, 2010. ,
Ownership types for flexible alias protection, Object-Oriented Programming, Systems , Languages, and Applications (OOPSLA), pp.48-64, 1998. ,
Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.262-275, 1999. ,
DOI : 10.1145/292540.292564
Enforcing high-level protocols in low-level software, Programming Language Design and Implementation (PLDI), pp.59-69, 2001. ,
Typestates for Objects, European Conference on Object-Oriented Programming, pp.465-490, 2004. ,
DOI : 10.1007/978-3-540-24851-4_21
Universes: Lightweight Ownership for JML., The Journal of Object Technology, vol.4, issue.8, pp.5-32, 2005. ,
DOI : 10.5381/jot.2005.4.8.a1
Language support for fast and reliable message-based communication in Singularity OS, EuroSys, pp.177-190, 2006. ,
Adoption and focus: practical linear types for imperative programming, Programming Language Design and Implementation (PLDI), pp.13-24, 2002. ,
Uniqueness and reference immutability for safe parallelism, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.21-40, 2012. ,
Local Reasoning for Storable Locks and Threads, 2007. ,
DOI : 10.1007/978-3-540-76637-7_3
Oracle Semantics for Concurrent Separation Logic, European Symposium on Programming (ESOP), pp.353-367, 2008. ,
DOI : 10.1007/978-3-540-78739-6_27
The VeriFast program verifier, 2008. ,
Extended alias type system using separating implication, Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '11, 2011. ,
DOI : 10.1145/1929553.1929559
A functional representation of data structures with a hole, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.75-84, 1998. ,
DOI : 10.1145/268946.268953
Ownership transfer in universe types, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp.461-478, 2007. ,
A type system for borrowing permissions, Principles of Programming Languages (POPL), pp.557-570, 2012. ,
Resources, concurrency and local reasoning, Theoretical Computer Science, vol.375, issue.13, pp.271-307, 2007. ,
Type soundness for Core Mezzo. Unpublished, 2013. ,
Programming with permissions in Mezzo (long version) Unpublished, 2013. ,
Separation logic: A logic for shared mutable data structures, Logic in Computer Science (LICS), pp.55-74, 2002. ,
Alias Types, European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pp.366-381, 2000. ,
DOI : 10.1007/3-540-46425-5_24
Secure distributed programming with value-dependent types, International Conference on Functional Programming (ICFP), pp.266-278, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00939188
Safe manual memory management in Cyclone, Science of Computer Programming, vol.62, issue.2, pp.122-144, 2006. ,
DOI : 10.1016/j.scico.2006.02.003
Practical affine types, Principles of Programming Languages (POPL), pp.447-458, 2011. ,
Local reasoning about while-loops. Unpublished, 2010. ,
Alias Types for Recursive Data Structures, Types in Compilation (TIC), volume 2071 of Lecture Notes in Computer Science, pp.177-206, 2000. ,
DOI : 10.1007/3-540-45332-6_7