copy the first half of the Iris appendix into the repository, so that we can...

copy the first half of the Iris appendix into the repository, so that we can keep the documentation in sync

LICENSE

-All files in this development are distributed under the terms of the BSD
-license, included below.
+All files in this development, excluding those in docs/, are distributed
+under the terms of the BSD license, included below.
 
 ------------------------------------------------------------------------------
 

docs/.gitignore

+*.pdf
+*.aux
+*.log
+*.out
+*.synctex.gz
+*.txss
+*.thm
+*.toc
+*.bbl
+*.blg
+*.bcf
+*.run.xml

docs/bib.bib

+
+
+@inproceedings{liang-feng,
+ author = {Liang, Hongjin and Feng, Xinyu},
+ title = {Modular Verification of Linearizability with Non-fixed Linearization Points},
+ booktitle = {PLDI},
+ year = {2013}
+} 
+
+@INPROCEEDINGS{hlrg,
+    author = {Ming Fu and Yong Li and Xinyu Feng and Zhong Shao and Yu Zhang},
+    title = {Reasoning about optimistic concurrency using a program logic for history},
+    booktitle = {CONCUR},
+    year = {2010}
+}
+
+@Book{Milner1999,
+	author={Robin Milner},
+	title={Communicating and Mobile Systems: the $\pi$-Calculus},
+	publisher={Cambridge University Press},
+	year={1999},
+}
+
+@article{Walker:IC1995,
+	Author = {David Walker},
+	Journal = {Inf. Comput.},
+	Number = {2},
+	Pages = {253--271},
+	Title = {Objects in the pi-Calculus},
+	Volume = {116},
+	Year = {1995}}
+
+@inproceedings{jensen-fsl,
+ author = {Jensen, Jonas Braband and Birkedal, Lars},
+ title = {Fictional Separation Logic},
+ booktitle = {ESOP},
+ year = {2012},
+} 
+
+@article{America-Rutten:JCSS89,
+	Author = {Pierre America and Jan Rutten},
+	Journal = {J. Comput. Syst. Sci.},
+	Number = {3},
+	Pages = {343--375},
+	Title = {Solving Reflexive Domain Equations in a Category of Complete Metric Spaces},
+	Volume = {39},
+	Year = {1989}}
+
+@Misc{Sieczkowski+:tutorial14,
+  author = 	 {Filip Sieczkowski and Ale\v{s} Bizjak and Yannick Zakowski and Lars Birkedal},
+  title = 	 {Modular Reasoning about Concurrent Higher-Order Imperative Programs: a {Coq} Tutorial},
+  howpublished = {\url{http://users-cs.au.dk/birke/modures/tutorial/index.html}},
+  year = 	 2014
+}
+
+@inproceedings{birkedal:popl11,
+ author    = "Lars Birkedal and Bernhard Reus and Jan Schwinghammer and Kristian St{\o}vring and Jacob Thamsborg and Hongseok Yang",
+ title     = "Step-Indexed {Kripke} Models over Recursive Worlds",
+ booktitle = "POPL",
+ year = 2011,
+}
+                  
+@inproceedings{parkinson+:popl08,
+ author    = "Matthew Parkinson and Gavin Bierman",
+ title     = "Separation Logic, Abstraction and Inheritance",
+ booktitle = "POPL",
+ year = 2008,
+}
+
+@Unpublished{mogelberg:2009,
+  author = 	 {Rasmus E. M{\o}gelberg},
+  title = 	 {A Nominal Relational Model for Local Variables},
+  note = 	 {Manuscript},
+  month = 	 {may},
+  year = 	 2009,
+  annote = 	 {Available at: \url{http://www.itu.dk/people/mogel/papers/nom-rel-model.pdf}}
+}
+
+@InProceedings{mogelberg-simpson:07,
+  author = 	 {Rasmus E. M{\o}gelberg and Alex Simpson},
+  title = 	 {Relational Parametricity for Computational Effects},
+  booktitle = {LICS},
+  year = 	 2007}
+
+@inproceedings{parkinson05,
+ author = {M. J. Parkinson and  G. M. Bierman},
+ title = {Separation logic and abstraction},
+ booktitle = {POPL},
+ year = {2005},
+ pages = {247--258},
+}
+
+@phdthesis{parkinson_thesis,
+ author    = "Matthew Parkinson",
+ title     = "Local Reasoning for Java",
+ school    = "University of Cambridge",
+ month     = "November",
+ year      = "2005"
+}
+
+
+@Article{honsell+:variable-typed,
+  author = 	 {Furio Honsell and Ian A. Mason and Scott Smith and Carolyn Talcott},
+  title = 	 {A Variable Typed Logic of Effects},
+  journal = 	 {Inf. Comput.},
+  year = 	 {1995},
+  volume = 	 {119},
+  number = 	 {1},
+  pages = 	 {55--90},
+}
+
+@article{sumii-pierce:jacm,
+ author = {Eijiro Sumii and Benjamin Pierce},
+ title = {A Bisimulation for Type Abstraction and Recursion},
+ journal = {JACM},
+ volume = 54,
+ number = 5,
+ year = 2007,
+ pages = {1--43},
+}
+
+@inproceedings{banerjee-naumann:ecoop05,
+  author = "Anindya Banerjee and David A. Naumann",
+  title = "State based ownership, reentrance, and encapsulation",
+  booktitle = {ECOOP},
+  year = 2005,
+}
+
+@InProceedings{koutavas-wand:popl06,
+  author = 	 {Vasileios Koutavas and Mitchell Wand},
+  title = 	 {Small Bisimulations for Reasoning About Higher-Order Imperative Programs},
+  booktitle = 	 {POPL},
+  year = 	 {2006},
+}
+
+@Misc{appendix,
+  title = 	 {Appendix and {Coq} development},
+  note = 	 {\url{http://plv.mpi-sws.org/iris}},
+}
+
+
+@inproceedings{dreyer+:icfp10,
+  author = 	 {Derek Dreyer and Georg Neis and Lars Birkedal},
+  title = 	 {The Impact of Higher-Order State and Control Effects on Local Relational Reasoning},
+  year = 2010,
+  booktitle = {ICFP},
+}
+
+@InProceedings{thamsborg+:icfp11,
+  author = 	 {Jacob Thamsborg and Lars Birkedal},
+  title = 	 {A {Kripke} Logical Relation for Effect-Based Program Transformations},
+  booktitle = {ICFP},
+  year = 2011,
+}
+
+@inproceedings{hur+:popl11,
+  author =       {Chung-Kil Hur and Derek Dreyer},
+  title = 	 {A {Kripke} Logical Relation Between {ML} and Assembly},
+  year = 	 {2011},
+  booktitle = {POPL},
+}
+
+@inproceedings{nakano:lics00,
+  author = "Hiroshi Nakano",
+  title = {A modality for recursion},
+  booktitle = {LICS},
+  year = "2000",
+}
+
+
+
+@InProceedings{birkedal+:fossacs09,
+  author = 	 {Lars Birkedal and Kristian St\o{}vring and Jacob Thamsborg},
+  title = 	 {Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types},
+  booktitle = {FOSSACS},
+  year = 	 {2009},
+}
+
+@inproceedings{plotkin-abadi,
+    AUTHOR = {Gordon Plotkin and Mart\'in Abadi},
+     TITLE = {A logic for parametric polymorphism},
+ BOOKTITLE = {TLCA},
+     year = 1993,
+}
+
+@InCollection{pitts:attapl,
+  author =	 {Andrew Pitts},
+  title =	 {Typed Operational Reasoning},
+  booktitle =	 {Advanced Topics in Types and Programming Languages},
+  year =	 2005,
+  publisher =    {MIT Press},
+  chapter =      {7},
+  editor =	 {B. C. Pierce},
+}
+
+                  
+
+@Article{yoshida+:lmcs08,
+  author = 	 {Nobuko Yoshida and Kohei Honda and Martin Berger},
+  title = 	 {Logical Reasoning for Higher-Order Functions with Local State},
+  journal = 	 {LMCS},
+  year = 	 {2008},
+  volume = 	 {4},
+  number = 	 {4:2},
+}
+
+@Article{BirkedalL:semslt-lmcs,
+  author = 	 {L. Birkedal and N. Torp-Smith and H. Yang},
+  title = 	 {Semantics of Separation-logic Typing and Higher-order Frame Rules for {Algol}-like Languages},
+  journal =      {LMCS},
+  volume =          {2},
+  number =       {5:1},
+  year = 	 2006,
+}
+                  @Article{BirkedalL:parsepl-journal,
+  author = 	 {L. Birkedal and H. Yang},
+  title = 	 {Relational Parametricity and Separation Logic},
+  journal = 	 {Logical Methods in Computer Science},
+  year = 	 2008,
+  volume = 	 4,
+  number = 	 {2:6},
+  pages = 	 {1--27},
+  month = 	 {may}}
+
+
+
+@InProceedings{BirkedalL:bihsl,
+  author = 	 {B. Biering and L. Birkedal and N. Torp-Smith},
+  title = 	 {BI Hyperdoctrines and Higher-order Separation Logic},
+  booktitle =	 {ESOP},
+  year =	 2005,
+}
+
+@InProceedings{Schwinghammer-nested-triples-conf,
+  author = 	 {J. Schwinghammer and L. Birkedal and B. Reus and H. Yang},
+  title = 	 {Nested {H}oare Triples and Frame Rules for Higher-order Store},
+  booktitle =    {CSL},
+  year = 	 2009,
+}
+
+@inproceedings{krishnaswami-tldi09,
+  author    = {Neelakantan R. Krishnaswami and
+               Jonathan Aldrich and
+               Lars Birkedal and
+               Kasper Svendsen and
+               Alexandre Buisse},
+  title     = {Design patterns in separation logic},
+  booktitle = {TLDI},
+  year      = {2009},
+}
+
+@inproceedings{nanevski+:esop07,
+  author    = {Aleksandar Nanevski and
+               Amal Ahmed and
+               Greg Morrisett and
+               Lars Birkedal},
+  title     = {Abstract Predicates and Mutable {ADTs in Hoare Type Theory}},
+  booktitle = {ESOP},
+  year      = {2007},
+}
+
+@inproceedings{petersen-htt,
+  author    = {Rasmus Lerchedahl Petersen and
+               Lars Birkedal and
+               Aleksandar Nanevski and
+               Greg Morrisett},
+  title     = {A Realizability Model for Impredicative {H}oare Type Theory},
+  booktitle = {ESOP},
+  year      = {2008},
+}
+
+@InProceedings{ohearn+:popl04,
+  author =	"Peter W. O'Hearn and Hongseok Yang and John C.
+		 Reynolds",
+  title =	"Separation and Information Hiding",
+  booktitle =	"POPL",
+  year = 	"2004",
+}
+
+@InProceedings{Birkedal:Reus:Schwinghammer:Yang:08,
+  author =	"Lars Birkedal and Bernhard Reus and Jan Schwinghammer and Hongseok Yang",
+  title =	"A Simple Model of Separation Logic for Higher-order Store",
+  booktitle = "{ICALP'08}",
+  pages =	"348--360",
+  year = "2008"
+}
+
+@InProceedings{Banerjee:Naumann:Rosenberg:08,
+  author =	"Anindya Banerjee and David Naumann and Stan Rosenberg",
+  title =	"Regional Logic for Local Reasoning about Global Invariants",
+  booktitle =	"ECOOP",
+  year = 	"2008",
+  url =	"\url{http://www.cs.stevens.edu/~naumann/publications/node2.html}",
+}
+
+
+
+@Article{yang:relational,
+  title =	"Relational Separation Logic",
+  author =	"Hongseok Yang",
+  journal =	"TCS",
+  year = 	"2007",
+  number =	"1--3",
+  volume =	"375",
+  pages =	"308--334",
+}
+
+@IProceedings{birkedal+:ho-frame-rules,
+  author = 	 {Lars Birkedal and Noah Torp-Smith and Hongseok Yang},
+  title = 	 {Semantics of Separation-logic Typing and
+                  Higher-order Frame Rules},
+  booktitle =    {Proc. of LICS'05},
+  year = 	 {2005},
+  pages =        {260-269}
+}
+
+@InProceedings{aydemir+:popl08,
+  author = 	 {Brian Aydemir and Arthur Chargu\'{e}raud and Benjamin C. Pierce and Randy Pollack and Stephanie Weirich},
+  title = 	 {Engineering Formal Metatheory},
+  booktitle = "POPL",
+  year = 2008
+}
+
+@Article{birkedal+:lmcs06,
+  author = 	 {Lars Birkedal and Noah Torp-Smith and Hongseok Yang},
+  title = 	 {Semantics of Separation-logic Typing and
+                  Higher-order Frame Rules},
+  journal = 	 {LMCS},
+  year = 	 {2006},
+  volume = 	 {2},
+  number = 	 {5:1},
+}
+
+@Article{birkedal-yang,
+  author = 	 {Lars Birkedal and Hongseok Yang},
+  title = 	 {Relational Parametricity and Separation Logic},
+  journal = 	 {LMCS},
+  year = 	 {2008},
+  volume = 	 {4},
+  number = 	 {2:6},
+}
+
+@Article{reynolds:types,
+  author =   {John C. Reynolds},
+  title =    {Types, Abstraction, and Parametric Polymorphism},
+  journal =      {Information Processing},
+  year =     1983,
+}
+
+@inproceedings{reynolds:separation,
+  author = "John C. Reynolds",
+  title = "Separation logic: A logic for shared mutable data structures",
+  booktitle = "LICS",
+  year = "2002",
+}
+
+@InProceedings{birkedal-yang-fossacs,
+  title =	"Relational Parametricity and Separation Logic",
+  author =	"Lars Birkedal and Hongseok Yang",
+  year = 	"2007",
+  booktitle =	"FOSSACS",
+  pages =	"",
+  volume =	"4423",
+  series =	"Lecture Notes in Computer Science",
+  editor =	"Helmut Seidl",
+}
+
+@InProceedings{reus-schwinghammer:csl06,
+  author = 	 {Bernhard Reus and Jan Schwinghammer},
+  title = 	 {Separation Logic for Higher-order Store},
+  booktitle =	 {CSL},
+  year =	 "2006",
+}
+
+@InProceedings{Birkedal:Torp-Smith:Reynolds:04,
+  author =	"Lars Birkedal and Noah Torp-Smith and John C.
+		 Reynolds",
+  title =	"Local Reasoning about a Copying Garbage Collector",
+  booktitle =	"Conference Record of the 31st Annual {ACM}
+		 Symposium on Principles of Programming Languages",
+  publisher =	"ACM Press",
+  year = 	2004,
+  series =	"ACM SIGPLAN Notices",
+  pages =	"220--231",
+}
+
+@InProceedings{Thielecke:06,
+  author =	"Hayo Thielecke",
+  title =	"Frame rules from answer types for code pointers",
+  booktitle =    "Conference Record of the 33rd Annual ACM Symposium on
+                 Principles of Programming Languages",
+  publisher =	"ACM Press",
+  pages =	"309--319",
+  year = 	2006,
+}
+
+
+@Article{Reus:Schwinghammer:MSCS,
+  author = 	 {Bernhard Reus and Jan Schwinghammer},
+  title = 	 {Denotational Semantics for a Program Logic of Objects},
+  journal = 	 {Mathematical Structures in Computer Science},
+  year = 	 2006,
+  volume =	 16,
+  number =	 2,
+  pages =	 {313--358},
+  month =	 {April},
+}
+
+@InProceedings{Reus:Streicher:05,
+  author = 	 {Bernhard Reus and Thomas Streicher},
+  title = 	 {About {Hoare} Logics for Higher-Order Store},
+  booktitle =	 {International Colloquium on Automata,
+		 Languages and Programming (ICALP'05)},
+pages =	"1337--1348",
+  year =	 2005,
+  series =	 {Lecture Notes in Computer Science},
+  publisher =	 {Springer}
+}
+
+@InProceedings{Reddy:88,
+  author =       "Uday S. Reddy",
+  title =	"Objects as Closures: Abstract Semantics of
+		 Object-oriented Languages",
+  pages =	"289--297",
+  editor =       "Jerome Chailloux",
+  booktitle =    "Proceedings of the {ACM} Conference on {LISP} and
+		 Functional Programming",
+  month =	jul,
+  year =	 1988,
+  publisher =    "ACM Press",
+}
+
+@InCollection{OHearn:Tennent:92,
+  author =	"Peter W. O'Hearn and Robert D. Tennent",
+  title =	"Semantics of Local Variables",
+  pages =	"217--238",
+  booktitle =	"Applications of Categories in Computer Science",
+  editor =	"M. P. Fourman and P. T. Johnstone and A. M. Pitts",
+  year = 	"1992",
+  publisher =	"Cambridge University Press",
+  series =	"London Mathematical Society Lecture Note Series",
+  volume =	"177",
+}
+
+@InProceedings{Morrisett:Ahmed:Fluet,
+  author = 	 {Greg Morrisett and Amal Ahmed and Matthew Fluet},
+  title = 	 {L3: A Linear Language with Locations},
+  booktitle =	 {Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA '05)},
+  year =	 2005,
+  volume =	 3461,
+  series =	 {Lecture Notes in Computer Science},
+  publisher =	 {Springer}
+}
+
+@InProceedings{Ahmed:Fluet:Morrisett:05,
+  author = 	 {Amal Ahmed and Matthew Fluet and Greg Morrisett},
+  title = 	 {A Step-Indexed Model of Substructural State},
+  booktitle =	 {Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP '05)},
+  year =	 2005,
+  note =	 {To appear}
+}
+
+@TechReport{Aboul-Hosn:Kozen:05,
+  author = 	 {Kamal Aboul-Hosn and Dexter Kozen},
+  title = 	 {Relational Semantics of Local Variable Scoping},
+  institution =  {Computer Science Department, Cornell University},
+  year = 	 2005,
+  number =	 {2005-2000},
+  month =	 jul,
+}
+
+@Article{Abadi:Cardelli:95,
+  author =       "Mart{\'\i}n Abadi and Luca Cardelli",
+  title =        "A theory of primitive objects: Second-order systems",
+  journal =      "Science of Computer Programming",
+  volume =       "25",
+  number =       "2-3",
+  pages =        "81--116",
+  month =        dec,
+  year =         "1995",
+}
+
+@Book{Davey:Priestley:02,
+  author =       "Brian A. Davey and Hilary A. Priestley",
+  publisher =    "Cambridge University Press",
+  title =        "Introduction to Lattices and Order",
+  edition =      "Second",
+  year =         2002,
+}
+
+@Article{Mason:Smith:Talcott:96,
+  author =       "Ian A. Mason and Scott F. Smith and Carolyn L.
+                 Talcott",
+  title =        "From Operational Semantics to Domain Theory",
+  journal =      "Information and Computation",
+  volume =       "128",
+  number =       "1",
+  year =         "1996",
+  pages =        "26--47",
+}
+
+@InCollection{Talcott:98,
+  author =       "Carolyn L. Talcott",
+  title =        "Reasoning about Functions with Effects",
+  pages =        "347--390",
+  editor =       "Andrew D. Gordon and Andrew M. Pitts",
+  booktitle =    "Higher Order Operational Techniques in Semantics",
+  publisher =    "Cambridge University Press",
+  series =       "Publications of the Newton Institute",
+  year =         "1998",
+}
+
+
+@Book{Abadi:Cardelli:96,
+  author =       "Mart{\'\i}n Abadi and Luca Cardelli",
+  title =        "A Theory of Objects",
+  publisher =    "Springer",
+  year =         "1996",
+}
+
+@Article{Abadi:Cardelli:96a,
+  title =        "A Theory of Primitive Objects: Untyped and First-Order
+                 Systems",
+  author =       "Mart{\'\i}n Abadi and Luca Cardelli",
+  pages =        "78--102",
+  journal =      "Information and Computation",
+  month =        mar,
+  year =         "1996",
+  volume =       "125",
+  number =       "2",
+}
+
+@InProceedings{Mitchell:84,
+  author =       "John C. Mitchell",
+  title =        "Coercion and type inference",
+  booktitle =    "Conference Record of the 11th Annual ACM Symposium on
+                 Principles of Programming Languages",
+  pages =        "175--185",
+  publisher = "ACM Press",
+  month =        jan,
+  year =         1984,
+}
+
+
+@InProceedings{Reynolds:80,
+  author =       "John C. Reynolds",
+  title =        "Using category theory to design implicit conversions
+                 and generic operators",
+  booktitle =    "Proceedings of the Aarhus Workshop on
+                 Semantics-Directed Compiler Generation",
+  editor =       "Neil D. Jones",
+  month =        jan,
+  year =         1980,
+  publisher =    "Springer",
+  series =       "Lecture Notes in Computer Science",
+  number =       94,
+  pages = "211--258",
+}
+
+@Article{OHearn:Reynolds:00,
+  author =       "Peter W. O'Hearn and John C. Reynolds",
+  title =        "From Algol to Polymorphic Linear Lambda-calculus",
+  journal =      "Journal of the  ACM",
+  volume =       "47",
+  number =       "1",
+  pages =        "167--223",
+  month =        jan,
+  year =         "2000",
+}
+
+
+@InProceedings{Abadi:Cardelli:Curien:93,
+  author =       "Mart\'{\i}n Abadi and Luca Cardelli and Pierre-Louis Curien",
+  title =        "Formal Parametric Polymorphism",
+  booktitle =    "Conference Record of the 20th Annual ACM
+                 SIGPLAN-SIGACT Symposium on Principles of Programming
+                 Languages",
+  pages =        "157--170",
+  year =         "1993",
+}
+
+@InProceedings{Abadi:Cardelli:Plotkin:94,
+  author =       "Gordon D. Plotkin and Mart\'{\i}n Abadi and Luca
+                 Cardelli",
+  title =        "Subtyping and Parametricity",
+  booktitle =    "Proceedings of 9th Annual IEEE Symposium on Logic in Computer
+                 Science",
+  pages =        "310--319",
+  month =        jul,
+  year =         "1994",
+  publisher = {IEEE Computer Society Press},
+}
+
+@InProceedings{Abadi:Cardelli:Viswanathan:96,
+  author =       "Mart{\'\i}n Abadi and Luca Cardelli and Ramesh
+                 Viswanathan",
+  title =        "An interpretation of objects and object types",
+  booktitle =    "Conference record of the 23rd Symposium on Principles of Programming Languages",
+  year =         "1996",
+  pages =        "396--409",
+  publisher = {{ACM} Press},
+}
+
+
+
+
+
+
+@InProceedings{Abadi:Leino:97,
+  author = 	 {Mart{\'\i}n Abadi and K.~R.~M.~Leino},
+  title = 	 {A Logic of Object-oriented Programs},
+  booktitle = 	 {Proceedings of Theory and Practice of Software Development},
+  pages = 	 {682--696},
+  year = 	 {1997},
+  editor = 	 {Michel Bidoit and Max Dauchet},
+  volume = 	 {1214},