FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES, International Journal of Foundations of Computer Science, vol.02, issue.01, pp.1-21, 1991. ,
DOI : 10.1142/S0129054191000029
L 3 : A linear language with locations, Fundamenta Informaticae, vol.77, issue.4, pp.397-449, 2007. ,
Semantic foundations for typed assembly languages, ACM Transactions on Programming Languages and Systems, vol.32, issue.3, 2010. ,
DOI : 10.1145/1709093.1709094
A step-indexed model of substructural state, Pages 78?91 of: ACM International Conference on Functional Programming (ICFP), 2005. ,
Semantics of types for mutable state, 2004. ,
Balloon types: Controlling sharing of state in data types, Pages 32?59 of: European Conference on Object-Oriented Programming, 1997. ,
DOI : 10.1007/BFb0053373
Subtyping recursive types, ACM Transactions on Programming Languages and Systems, vol.15, issue.4, pp.575-631, 1993. ,
DOI : 10.1145/155183.155231
URL : https://hal.archives-ouvertes.fr/inria-00070035
Amortised resource analysis with separation logic, Pages 85?103 of: European Symposium on Programming (ESOP), 2010. ,
Mechanized Metatheory for the Masses: The PoplMark Challenge, Pages 50?65 of: International Conference on Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science, 2005. ,
DOI : 10.1007/11541868_4
Dual intuitionistic linear logic, 1996. ,
Comparing semantic and syntactic methods in mechanized proof frameworks, International Workshop on Proof-Carrying Code (PCC), 2008. ,
Modular typestate checking of aliased objects, Pages 301?320 of: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2007. ,
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages, Logical Methods in Computer Science, vol.2, issue.5, 2006. ,
DOI : 10.2168/LMCS-2(5:1)2006
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, 2009. ,
DOI : 10.1137/0211062
Realisability semantics of parametric polymorphism, general references and recursive types, Mathematical Structures in Computer Science, vol.4960, issue.04, pp.655-703, 2010. ,
DOI : 10.1137/0211062
Step-indexed Kripke models over recursive worlds, Pages 119?132 of: ACM Symposium on Principles of Programming Languages (POPL), 2011. ,
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Mathematical Structures in Computer Science, vol.37, issue.04, pp.827-859, 2011. ,
DOI : 10.1016/S0890-5401(03)00011-7
URL : https://hal.archives-ouvertes.fr/inria-00543157
Ownership types for safe programming: preventing data races and deadlocks, Pages 211?230 of: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2002. ,
Semantics of fractional permissions with nesting, ACM Transactions on Programming Languages and Systems, vol.32, issue.6, 2010. ,
DOI : 10.1145/1749608.1749611
Connecting effects and uniqueness with adoption, Pages 283?295 of: ACM Symposium on Principles of Programming Languages (POPL), 2005. ,
Coinductive axiomatization of recursive type equality and subtyping, Fundamenta Informaticae, vol.33, pp.309-338, 1998. ,
DOI : 10.1007/3-540-62688-3_29
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
Local Action and Abstract Separation Logic, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007. ,
DOI : 10.1109/LICS.2007.30
The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, pp.363-408, 2012. ,
DOI : 10.1007/s10817-011-9225-2
Functional translation of a calculus of capabilities, Pages 213?224 of: ACM International Conference on Functional Programming (ICFP), 2008. ,
Ownership types for flexible alias protection, Pages 48?64 of: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 1998. ,
Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, 1999. ,
DOI : 10.1145/292540.292564
Subtyping, declaratively. Pages 100?118 of: International Conference on Mathematics of Program Construction (MPC), Lecture Notes in Computer Science, vol.6120, 2010. ,
Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem, Indag. Math, vol.34, issue.5, pp.381-392, 1972. ,
Enforcing high-level protocols in low-level software, Pages 59?69 of: ACM Conference on Programming Language Design and Implementation (PLDI), 2001. ,
Wrestling with rep exposure, 1998. ,
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
Concurrent Abstract Predicates, 2010. ,
DOI : 10.1007/978-3-642-14107-2_24
Views: compositional reasoning for concurrent programs, 2012. ,
A fresh look at separation algebras and share accounting. Pages 161?177 of: Asian Symposium on Programming Languages and Systems (APLAS), Lecture Notes in Computer Science, vol.5904, 2009. ,
Adoption and focus: practical linear types for imperative programming, Pages 13?24 of: ACM Conference on Programming Language Design and Implementation (PLDI), 2002. ,
Language support for fast and reliable message-based communication in Singularity OS, 2006. ,
Recursive subtyping revealed, Journal of Functional Programming, vol.12, issue.6, pp.511-548, 2002. ,
Numbering matters: First-order canonical forms for second-order recursive types, Pages 150?161 of: ACM International Conference on Functional Programming (ICFP), 2004. ,
Report on the FX-91 programming language, 1992. ,
Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse d'état, 1972. ,
A Theory of Second-Order Trees, Pages 147?161 of: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, 2002. ,
DOI : 10.1007/3-540-45927-8_11
Local Reasoning for Storable Locks and Threads, 2007. ,
DOI : 10.1007/978-3-540-76637-7_3
A simplified account of polymorphic references, Information Processing Letters, vol.51, issue.4, pp.201-206, 1994. ,
DOI : 10.1016/0020-0190(94)90120-1
Proof of correctness of data representations, Acta Informatica, vol.4, pp.271-281, 1972. ,
Oracle Semantics for Concurrent Separation Logic, Pages 353?367 of: European Symposium on Programming (ESOP), 2008. ,
DOI : 10.1007/978-3-540-78739-6_27
A type system for bounded space and functional in-place update, Nordic Journal of Computing, vol.7, issue.4, pp.258-289, 2000. ,
Islands: Aliasing protection in object-oriented languages, Pages 271?285 of: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 1991. ,
BI as an assertion language for mutable data structures, Pages 14?26 of: ACM Symposium on Principles of Programming Languages (POPL), 2001. ,
State in Haskell, LISP and Symbolic Computation, vol.2, issue.4, pp.293-341, 1995. ,
DOI : 10.1007/BF01018827
Possible World Semantics for General Storage in Call-By-Value, Computer Science Logic. Lecture Notes in Computer Science, vol.2471, 2002. ,
DOI : 10.1007/3-540-45793-3_16
An ideal model for recursive polymorphic types, Information and Control, vol.71, issue.1-2, pp.95-130, 1986. ,
DOI : 10.1016/S0019-9958(86)80019-5
Lightweight linear types in system F ? . Pages 77?88 of: Workshop on Types in Language Design and Implementation (TLDI), 2010. ,
Polymorphic type inference and containment, Information and Computation, vol.76, issue.2-3, pp.2-3, 1988. ,
DOI : 10.1016/0890-5401(88)90009-0
Statically tracking state with typed regions, 2008. ,
Universes: A type system for alias and dependency control, 2001. ,
Hoare type theory, polymorphism and separation, Journal of Functional Programming, vol.18, pp.5-6, 2008. ,
Structuring the verification of heap-manipulating programs, Pages 261?274 of: ACM Symposium on Principles of Programming Languages (POPL), 2010. ,
Resources, concurrency and local reasoning, Theoretical Computer Science, vol.375, pp.1-3, 2007. ,
Separation and information hiding, Pages 268?280 of: ACM Symposium on Principles of Programming Languages (POPL), 2004. ,
Imperative functional programming, Pages 71?84 of: ACM Symposium on Principles of Programming Languages (POPL), 1993. ,
The essence of monotonic state, Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '11, 2011. ,
DOI : 10.1145/1929553.1929565
URL : https://hal.archives-ouvertes.fr/hal-01081193
A Canonical Locally Named Representation of Binding, Journal of Automated Reasoning, vol.40, issue.4, pp.185-207, 2012. ,
DOI : 10.1007/s10817-011-9229-y
Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008. ,
DOI : 10.1109/LICS.2008.16
Generalizing the higher-order frame and anti-frame rules, 2009. ,
Three comments on the anti-frame rule, 2009. ,
Accompanying Coq scripts; for browsing, 2012. ,
Accompanying Coq scripts; for downloading Available at http: //gallium.inria.fr/~fpottier/ssphs/ssphs.tar.gz and also as an online supplement at http, 2012. ,
Programming with permissions: an introduction to Mezzo, 2012. ,
Separation logic for higher-order store. Pages 575?590 of: Computer Science Logic, Lecture Notes in Computer Science, vol.4207, 2006. ,
Towards a theory of type structure. Pages 408?425 of: Colloque sur la Programmation, Lecture Notes in Computer Science, vol.19, 1974. ,
Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002. ,
DOI : 10.1109/LICS.2002.1029817
Nested Hoare triples and frame rules for higher-order store. Pages 440?454 of: Computer Science Logic, Lecture Notes in Computer Science, vol.5771, 2009. ,
A Semantic Foundation for Hidden State, Pages 2?17 of: International Conference on Foundations of Software Science and Computation Structures (FOSSACS). Lecture Notes in Computer Science, 2010. ,
DOI : 10.1007/978-3-642-12032-9_2
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces, pp.305-319, 2011. ,
DOI : 10.1007/978-3-642-19805-2_21
A step-indexed Kripke model of hidden state, Mathematical Structures in Computer Science, 2012. ,
DOI : 10.1145/504709.504712
URL : https://hal.archives-ouvertes.fr/hal-00772757
Alias Types, Pages 366?381 of: European Symposium on Programming (ESOP), 2000. ,
DOI : 10.1007/3-540-46425-5_24
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
The type and effect discipline, Information and Computation, vol.11, issue.2, pp.245-296, 1994. ,
Weak updates and separation logic. Pages 178?193 of: Asian Symposium on Programming Languages and Systems (APLAS), Lecture Notes in Computer Science, vol.5904, 2009. ,
Region-Based Memory Management, Information and Computation, vol.132, issue.2, pp.109-176, 1997. ,
DOI : 10.1006/inco.1996.2613
Stateful Contracts for Affine Types, Pages 550?569 of: European Symposium on Programming (ESOP), 2010. ,
DOI : 10.1007/978-3-642-11957-6_29
Nominal Techniques in Isabelle/HOL, Journal of Automated Reasoning, vol.323, issue.1???2, pp.327-356, 2008. ,
DOI : 10.1007/s10817-008-9097-2
Semantic types: a fresh look at the ideal model for types, Pages 52?63 of: ACM Symposium on Principles of Programming Languages (POPL), 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00150968
Substructural type systems Advanced Topics in Types and Programming Languages, pp.3-43, 2005. ,
Alias types for recursive data structures. Pages 177?206 of: Workshop on Types in Compilation (TIC), Lecture Notes in Computer Science, vol.2071, 2000. ,
Simple imperative polymorphism, Lisp and Symbolic Computation, pp.343-356, 1995. ,
DOI : 10.1007/BF01018828
A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994. ,
DOI : 10.1006/inco.1994.1093