@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},
pages = {388--402},
}
@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 = {JCSS},
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. {Anonymous} supplementary material submitted with the paper.},
key = {A}
}
@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},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
}
@InProceedings{Abadi:Pierce:Plotkin:89,
author = "Mart\'{\i}n Abadi and Benjamin C. Pierce and Gordon D. Plotkin",
title = "Faithful Ideal Models for Recursive Polymorphic Types",
booktitle = "Proceedings of 4th Annual IEEE Symposium on Logic in Computer Science",
pages = "216--225",
month = jun,
year = "1989",
publisher = {IEEE Computer Society Press},
}
@InProceedings{Abadi:Plotkin:90,
author = {Mart\'{\i}n Abadi and Gordon D. Plotkin},
title = {A PER Model of Polymorphism and Recursive Types},
booktitle = {Proceedings of 5th Annual IEEE Symposium on Logic in Computer Science},
pages = {355--365},
year = {1990},
publisher = {IEEE Computer Society Press},
}
@InProceedings{Abadi:Plotkin:93,
author = "Gordon D. Plotkin and Mart\'{\i}n Abadi",
title = "A logic for parametric polymorphism",
booktitle = "International Conference on Typed Lambda Calculi and
Applications",
year = "1993",
editor = "M. Bezem and J. F. Groote",
series = "Lecture Notes in Computer Science",
number = "664",
pages = "361--375",
month = mar,
}
@InProceedings{Abramsky:Ghica:Murawski:Ong:Stark:04,
author = {Samson Abramsky and Dan Ghica and Andrzej Murawski and
Luke Ong and Ian Stark},
title = {Nominal Games and Full Abstraction for the
Nu-Calculus},
booktitle = {Proceedings of the 19th Annual IEEE Symposium on
Logic in Computer Science},
pages = {150--159},
year = 2004,
publisher = {IEEE Computer Society Press},
}
@InCollection{Abramsky:Jung:94,
author = {Samson Abramsky and Achim Jung},
booktitle = {Handbook of Logic in Computer Science},
title = {Domain Theory},
publisher = {Clarendon Press},
pages = {1--168},
year = 1994,
editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
volume = 3
}
@InProceedings{Abramsky:McCusker:97,
author = {Samson Abramsky and Guy McCusker},
title = {Game Semantics},
booktitle = {Logic and Computation. Proceedings of the 1997 Marktoberdorf Summer School},
year = {1998},
editor = {H. Schwichtenberg and U. Berger},
publisher = {Springer},
}
@InProceedings{Abramsky:McCusker:Honda:98,
title = "A Fully Abstract Game Semantics for General
References",
author = "Samson Abramsky and Kohei Honda and Guy {McCusker}",
booktitle = "Proceedings 13th Annual IEEE Symposium on Logic
in Computer Science",
publisher = "IEEE Computer Society Press",
pages = {334--344},
year = "1998",
}
@inproceedings{Aceto:Huettel:Ingolfsdottir:Kleist:00,
author = {Luca Aceto and Hans H{\"u}ttel and Anna Ing{\'o}lfsd{\'o}ttir and Josva Kleist},
title = {Relating semantic models for the object calculus},
booktitle = {Electronic Notes in Theoretical Computer Science},
volume = {7},
editor = {C. Palamidessi and J. Parrow},
year = {2000}
}
@InProceedings{Ahmed:Appel:Virga:02,
author = {Amal J. Ahmed and Andrew W. Appel and Roberto Virga},
title = {A Stratified Semantics of General References Embeddable in Higher-Order Logic},
booktitle = {Proceedings of 17th Annual IEEE Symposium Logic in Computer Science},
publisher = "IEEE Computer Society Press",
pages = {75--86},
year = {2002},
}
@Unpublished{Ahmed:Appel:Virga:03,
author = {Amal J. Ahmed and Andrew W. Appel and Roberto Virga},
title = {An Indexed Model of Impredicative Polymorphism and Mutable References},
note = {Princeton University},
month = {January},
year = {2003},
}
@Article{Amadio:91,
author = "R. M. Amadio",
title = "Recursion over realizability structures",
journal = "Information and Computation",
volume = "91",
number = "1",
pages = "55--86",
year = "1991",
}
@InProceedings{Amadio:Cardelli:91,
author = "Roberto M. Amadio and Luca Cardelli",
title = "Subtyping Recursive Types",
pages = "104--118",
booktitle = "Conference Record of the 18th Annual {ACM} Symposium
on Principles of Programming Languages",
month = jan,
year = "1991",
note = "Journal version in \cite{Amadio:Cardelli:93}",
}
@Article{Amadio:Cardelli:93,
author = "Roberto M. Amadio and Luca Cardelli",
title = "Subtyping Recursive Types",
journal = "ACM Transactions on Programming Languages and
Systems",
volume = "15",
number = "4",
pages = "575--631",
year = "1993",
}
@inProceedings{Andersen:Pedersen:Huettel:Kleist:97,
author = "Dan S. Andersen and Lars H. Pedersen and Hans H{\"u}ttel and Josva Kleist",
title = "Objects, Types and Modal Logics",
booktitle = "Proceedings of {FOOL4}",
year = "1997",
month = nov,
url = "citeseer.nj.nec.com/andersen96objects.html",
}
@inproceedings{mellies-vouillon,
author = "Paul-Andr{\'e} Melli{\`e}s and J{\'e}r{\^o}me Vouillon",
title = {Recursive polymorphic types and parametricity in an operational framework},
booktitle = {LICS},
year = "2005",
}
@Article{appel-mcallester,
author = {Andrew Appel and David McAllester},
title = {An Indexed Model of Recursive Types for Foundational Proof-Carrying Code},
journal = {TOPLAS},
year = {2001},
volume = {23},
number = {5},
pages = {657--683},
}
@InProceedings{appel+:vmm,
author = {Andrew Appel and Paul-Andr{\'e} Melli{\`e}s and Christopher Richards and J{\'e}r{\^o}me Vouillon},
title = {A Very Modal Model of a Modern, Major, General Type System},
booktitle = {POPL},
year = 2007
}
@InProceedings{dockins+:mfps08,
author = {Robert Dockins and Andrew W. Appel and Aquinas Hobor},
title = {Multimodal Separation Logic for Reasoning About Operational Semantics},
booktitle = {MFPS},
year = {2008},
}
@Article{Apt:Plotkin:86,
title = "Countable Nondeterminism and Random Assignment",
author = "Krzysztof R. Apt and Gordon D. Plotkin",
area = "Programming Languages and Systems",
pages = "724--767",
journal = "Journal of the ACM",
month = oct,
year = "1986",
volume = "33",
number = "4",
}
@Article{DiGianantonio:Honsell:Plotkin:95,
title = "Uncountable Limits and the lambda Calculus",
author = "Pietro {di Gianantonio} and Furio Honsell and Gordon D.
Plotkin",
journal = "Nordic Journal of Computing",
year = 1995,
number = 2,
volume = 2,
pages = "126--145",
}
@Article{Apt:81,
author = "Krzysztof R. Apt",
title = "Ten Years of {Hoare}'s Logic: {A} Survey --- Part
{I}",
journal = "ACM Transactions on Programming Languages and
Systems",
volume = "3",
number = "4",
pages = "431--483",
month = oct,
year = "1981",
}
@Book{Arnold:Gosling:Holmes:00,
author = "Ken Arnold and James Gosling and David Holmes",
key = "Arnold \& Gosling",
title = "The {Java} Programming Language",
publisher = "Addison-Wesley",
year = "2000",
edition = "Third",
}
@InProceedings{Banerjee:Naumann:02,
author = "Anindya Banerjee and David A. Naumann",
title = "Representation independence, confinement and access
control",
pages = "166--177",
month = jan,
year = "2002",
booktitle = "Proceedings of the 29th ACM SIGPLAN-SIGACT symposium
on Principles of Programming Languages",
publisher = "IEEE Computer Society Press",
}
@InCollection{Barendregt:92,
author = {Henk P. Barendregt},
title = {Lambda Calculi with Types},
booktitle = {Handbook of Logic in Computer Science},
pages = {117--309},
publisher = {Oxford University Press},
year = 1992,
editor = {Samson Abramsky and Dov Gabbay and T.~S.~E. Maibaum},
volume = 2,
chapter = 2
}
@InProceedings{ahmed:esop06,
author = {Amal Ahmed},
title = {Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types},
booktitle = {ESOP},
year = 2006,
}
@InProceedings{ahmed+:popl09,
author = {Amal Ahmed and Derek Dreyer and Andreas Rossberg},
title = {State-Dependent Representation Independence},
booktitle = {POPL},
year = {2009},
}
@InProceedings{dreyer+:lics09,
author = {Derek Dreyer and Amal Ahmed and Lars Birkedal},
title = {Logical Step-Indexed Logical Relations},
booktitle = {LICS},
year = {2009},
}
@InProceedings{benton:popl04,
author = {Nick Benton},
title = {Simple Relational Correctness Proofs for Static Analyses and Program Transformations},
booktitle = {POPL},
year = {2004},
}
@InProceedings{benton-leperchey,
author = {Nick Benton and Benjamin Leperchey},
title = {Relational Reasoning in a Nominal Semantics for Storage},
booktitle = {TLCA},
year = {2005},
}
@Article{Birkedal:Harper:99,
author = "Lars Birkedal and Robert W. Harper",
title = "Constructing interpretations of recursive types in an
operational setting",
journal = "Information and Computation",
year = "1999",
volume = "155",
pages = "3--63",
}
@Article{Blass:Gurevich:00,
author = "Andreas Blass and Yuri Gurevich",
title = "The Underlying Logic of {Hoare} Logic",
journal = "Bulletin of the European Association for Theoretical
Computer Science",
volume = "70",
pages = "82--110",
month = feb,
year = "2000",
url = "\url{http://research.microsoft.com/~gurevich/Opera/142.ps}",
}
@InProceedings{Bodirsky:Gaertner:Oertzen:Schwinghammer:01,
author = {Manuel Bodirsky and Tobias G\"artner and Timo von Oertzen and Jan Schwinghammer},
title = {Computing the Density of Regular Languages},
pages = {23--35},
month = aug,
address = {Helsinki},
booktitle = {Proceedings of the Student Session of the European Summer School in Logic, Language, and Information},
year = {2001},
}
@Misc{Bodirsky:Gaertner:Oertzen:Schwinghammer:LongRun,
author = {Manuel Bodirsky and Tobias G\"artner and Timo von Oertzen and Jan Schwinghammer},
year = {2002},
title = {Long-run properties of periodic probabilistic systems},
howpublished = {Manuscript},
}
@Misc{Bodirsky:Gaertner:Oertzen:Schwinghammer:Periods,
author = {Manuel Bodirsky and Tobias G\"artner and Timo von Oertzen and Jan Schwinghammer},
title = {Periodic Sequences of Group Elements},
year = {2002},
howpublished = {Manuscript},
}
@InProceedings{Bono:Bugliesi:99,
author = {Viviana Bono and Michele Bugliesi},
title = {Interpretations of Extensible Objects and Types},
booktitle = {Proceedings of the 12th Int. Symposium on Fundamentals of Computing},
pages = {112--123},
year = {1999},
volume = {1684},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
}
@InProceedings{Bono:Patel:Shmatikov:Mitchell:99,
author = "Viviana Bono and Amit J. Patel and Vitaly Shmatikov
and John C. Mitchell",
title = "A Core Calculus of Classes and Objects",
booktitle = "15th Conference on the Mathematical Foundations
of Programming Semantics",
series = "Electronic Notes in Computer Science",
volume = "20",
year = "1999",
month = apr,
}
@Article{Boudol:04,
author = {G{\'}erard Boudol},
title = {The recursive record semantics of objects revisited},
journal = {Journal of Functional Programming},
year = {2004},
volume = {14},
number = {3},
pages = {263-315},
month = may,
}
@Article{Bracha:Odersky:Stoutamire:Wadler:98,
author = "Gilad Bracha and Martin Odersky and David Stoutamire
and Philip Wadler",
title = "Making the Future Safe for the Past: Adding Genericity
to the {Java} Programming Language",
journal = "ACM SIG{\-}PLAN Notices",
volume = "33",
number = "10",
pages = "183--200",
month = oct,
year = "1998",
}
@InProceedings{Bracha:Ungar:04,
author = {Gilad Bracha and David Ungar},
title = {Mirrors: Design Principles for Meta-level Facilities of Object-Oriented Programming Languages},
booktitle = {Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications},
year = {2004},
month = oct,
publisher = {ACM Press},
}
@Article{Breazu-Tannen:EtAl:91,
author = "Val {Breazu-Tannen} and Thierry Coquand and Gunter
Gunter and Andre Scedrov",
title = "Inheritance as Implicit Coercion",
journal = "Information and Computation",
month = jul,
year = "1991",
number = "1",
volume = "93",
pages = "172--221",
}
@Book{Bruce:02,
author = "Kim B. Bruce",
title = "Foundations of Object-Oriented Languages: Types and
Semantics",
publisher = "MIT Press",
year = "2002",
}
@Article{Bruce:94,
author = "Kim B. Bruce",
title = "A Paradigmatic Object-Oriented Programming Language:
Design, Static Typing and Semantics",
journal = "Journal of Functional Programming",
volume = "4",
number = "2",
month = apr,
pages = "127--206",
year = "1994",
}
@article {Bruce:Cardelli:Pierce:99,
author = "Kim B. Bruce and Luca Cardelli and Benjamin C. Pierce",
title = "Comparing Object Encodings",
journal = "Information and Computation",
year = 1999,
month = nov,
volume = 155,
number = "1/2",
pages = "108--133",
}
@Article{Bruce:etal:95,
author = "Kim B. Bruce and Luca Cardelli and Giuseppe Castagna
and {The Hopkins Objects Group} and Gary T. Leavens and
Benjamin Pierce",
title = "On Binary Methods",
journal = "Theory and Practice of Object Systems",
publisher = "John Wiley and Sons, Inc.",
year = "1995",
pages = "221--242",
volume = "1",
number = "3",
}
@Book{Castagna:97,
author = "Giuseppe Castagna",
title = "Object-Oriented Programming: {A} Unified Foundation",
publisher = "Birkhauser",
year = 1997,
series = "Progress in Theoretical Computer Science",
}
@Article{Bugliesi:Delzanno:Liquori:Martelli:00,
author = "Michele Bugliesi and Giorgio Delzanno and Luigi Liquori and Maurizio Martelli",
title = "Object Calculi in Linear Logic",
journal = "Journal of Logic and Computation",
volume = 10,
number = 1,
pages = "75 --104",
month = feb,
year = "2000",
}
@InProceedings{Calcagno+:lics09,
author={Cristiano Calcagno and Peter W. O'Hearn and Hongseok Yang},
title={Local Action and Abstract Separation Logic},
booktitle={LICS},
year={2007},
}
@InProceedings{Calcagno:Ishtiaq:OHearn:00,
author = "Cristiano Calcagno and Samin Ishtiaq and Peter W.
O'Hearn",
title = "Semantic Analysis of Pointer Aliasing, Allocation and
Disposal in {H}oare Logic",
booktitle = "Proceedings of 2nd International Conference on Principles and
Practice of Declarative Programming",
year = "2000",
pages = "190--201",
editor = "Maurizio Gabbrielli and Frank Pfenning",
series = "Lecture Notes in Computer Science",
publisher = {Springer},
}
@InProceedings{Canning:Cook:Hill:Olthoff:Mitchell:89,
author = "P. Canning and W. Cook and W. Hill and W. Olthoff and
J. Mitchell",
title = "{F}-bounded polymorphism for object-oriented
programming",
booktitle = "Proceedings 4th International Conference on Functional Programming Languages and Computer
Architecture",
year = "1989",
publisher = "ACM Press",
pages = "273--280",
}
@InCollection{Cardelli:84,
author = "Luca Cardelli",
title = "A Semantics of Multiple Inheritance",
booktitle = "Semantics of Data Types",
editor = "Gilles Kahn and David MacQueen and Gordon Plotkin",
series = "Lecture Notes in Computer Science",
volume = "173",
pages = "51--67",
year = "1984",
month = jun,
publisher = "Springer",
abstract-url = "http://www.luca.demon.co.uk/Papers.html#Inheritance",
note = "Full version in \cite{Cardelli:88}"
}
@Article{Cardelli:88,
author = "Luca Cardelli",
title = "A Semantics of Multiple Inheritance",
journal = "Information and Computation",
volume = "76",
number = "2/3",
month = feb,
year = "1988",
pages = "138--164",
}
@Article{Cardelli:Martini:Mitchell:Scedrov:94,
author = "Luca Cardelli and Simone Martini and John C. Mitchell
and Andre Scedrov",
title = "An Extension of {S}ystem {F} with Subtyping",
journal = "Information and Computation",
volume = "109",
number = "1--2",
pages = "4--56",
year = "1994",
}
@Article{Cardelli:Wegner:85,
author = "Luca Cardelli and Peter Wegner",
title = "On Understanding Types, Data Abstraction, and
Polymorphism",
journal = "ACM Computing Surveys",
volume = "17",
number = "4",
pages = "471--522",
month = dec,
year = "1985",
}
@InProceedings{Cardone:89,
title = "Relational Semantics for Recursive Types and Bounded
Quantification",
author = "Felice Cardone",
editor = "Giorgio Ausiello and Mariangiola Dezani-Ciancaglini
and Simona Ronchi Della Rocca",
booktitle = "16th International Colloquium Automata, Languages and Programming",
month = jul,
year = "1989",
series = "Lecture Notes in Computer Science",
volume = "372",
publisher = "Springer",
pages = "164--178",
}
@Article{Clarke:79,
author = "E. M. Clarke",
year = "1979",
title = "Programming Language Constructs for which it it
Impossible to obtain good {Hoare} Axiom Systems",
journal = "Journal of the ACM",
volume = "26",
number = "1",
pages = "129--147",
}
@Article{Cook:78,
author = {Stephen A. Cook},
title = {Soundness and Completeness of an Axiom System for Program Verification},
journal = {{SIAM} Journal on Computing},
year = {1978},
volume = {7},
number = {1},
pages = {70--90},
}
@PhdThesis{Cook:89,
author = "William R. Cook",
title = "A Denotational Semantics of Inheritance",
school = "Department of Computer Science, Brown University",
type = "Ph.{D}. Thesis",
month = may,
year = "1989",
}
@Article{Cook:Palsberg:94,
author = "William Cook and Jens Palsberg",
title = "A Denotational Semantics of Inheritance and its
Correctness",
journal = "Information and Computation",
pages = "329--350",
year = "1994",
month = nov,
number = "2",
volume = "114",
}
@article{Coquand:Gunter:Winskel:89,
author = "Thierry Coquand and Carl A. Gunter and Glynn Winskel",
title = "Domain Theoretic Models of Polymorphism",
journal = "Information and Computation",
volume = "81",
number = "2",
pages = "123--167",
year = "1989",
url = "citeseer.nj.nec.com/coquand89domain.html"
}
@incollection{Cousot:90,
author = {Patrick Cousot},
title = {Methods and Logics for Proving Programs},
pages = {843--993},
editor = {Jan {van Leeuwen}},
chapter = 15,
booktitle = {Formal Models and Semantics},
volume = {B},
series = {Handbook of Theoretical Computer Science},
publisher = {Elsevier},
year = 1990,
}
@TechReport{Crary:99,
author = {Karl Crary},
title = {Simple, Efficient Object Encoding using Intersection Types},
institution = {Carnegie Mellon University},
year = {1999},
month = jan,
number = {CMU-CS-99-100},
}
@InCollection{Curien:Ghelli:94,
author = "Pierre-Louis Curien and Giorgio Ghelli",
title = "Coherence of Subsumption, Minimum Subtyping and
Type-Checking in ${F}_{\leq}$",
editor = "Carl A. Gunter and John C. Mitchell",
booktitle = "Theoretical Aspects of Object-Oriented Programming:
Types, Semantics, and Language Design",
series = "Foundations of Computing Series",
pages = "247--292",
publisher = "MIT Press",
year = "1994",
}
@InProceedings{Eifrig:Smith:Trifonov:95,
author = "Jonathan Eifrig and Scott Smith and Valery Trifonov",
title = "Type Inference for Recursively Constrained Types and
its Application to {OOP}",
booktitle = "Proceedings of the 1995 Mathematical Foundations of
Programming Semantics Conference",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Elsevier",
volume = "1",
year = "1995",
fullurl = "http://www.elsevier.nl/locate/entcs/volume1.html",
}
@Article{Eifrig:Smith:Trifonov:Zwarico:95,
author = "Jonathan Eifrig and Scott Smith and Valery Trifonov
and Amy Zwarico",
title = "An Interpretation of Typed {OOP} in a Language with
State",
journal = "Lisp and Symbolic Computation",
volume = 8,
number = 4,
pages = "357--397",
month = dec,
year = 1995,
}
@Article{Erkok:Launchbury:00,
author = "Levent Erk{\"o}k and John Launchbury",
title = "Recursive monadic bindings",
journal = "ACM SIG{\-}PLAN Notices",
volume = "35",
number = "9",
pages = "174--185",
month = sep,
year = "2000",
}
@MastersThesis{Fecher:99,
author = {Harald Fecher},
title = {Denotational Semantics of Untyped Object-Based Programming Languages},
school = {Technische Universit{\"a}t Darmstadt},
year = {1999},
}
@Article{Filinski:94,
author = "Andrzej Filinski",
title = "Recursion from Iteration",
journal = "{LISP} and Symbolic Computation",
volume = "7",
number = "1",
pages = "11--37",
month = jan,
year = "1994",
}
@InProceedings{Findler:Felleisen:01,
author = "Robert Bruce Findler and Matthias Felleisen",
title = "Contract Soundness for Object-Oriented Languages",
booktitle = "OOPSLA '01 Conference Proceedings",
year = "2001",
month = oct,
pages = "1--15",
}
@InProceedings{Findler:Felleisen:02,
author = {Robert Bruce Findler and Matthias Felleisen},
title = {Contracts for Higher-Order Functions},
booktitle = {Proceedings of the 2002 International Conference on Functional Programming},
OPTpages = {},
year = {2002},
OPTseries = {},
month = oct,
}
@Article{felleisen-hieb,
author = {Matthias Felleisen and Robert Hieb},
title = {The revised report on the syntactic theories of sequential control and state},
journal = {TCS},
year = {1992},
volume = {103},
number = {2},
pages = {235--271},
}
@PhdThesis{Fiore:94,
author = {Marcelo P. Fiore},
title = {Axiomatic Domain Theory in Categories of Partial Maps},
school = {University of Edinburgh},
year = {1994},
note = {LFCS report ECS-LFCS-94-307},
}
@Book{Fiore:96,
author = {Marcelo P. Fiore},
title = {Axiomatic Domain Theory in Categories of Partial Maps},
publisher = {Cambridge University Press},
year = 1996,
series = {Distinguished Dissertations in Computer Science}
}
@Article{FioreEtAl:96,
author = "Marcelo Fiore and Achim Jung and Eugenio Moggi and
Peter O'Hearn and Jon Riecke and Giuseppe Rosolini and
Ian Stark",
title = "Domains and Denotational Semantics: History,
Accomplishments and Open Problems",
journal = "Bulletin of the European Association for Theoretical
Computer Science",
volume = "59",
pages = "227--256",
month = jun,
year = "1996",
}
@Article{Fisher:Honsell:Mitchell:94,
author = "Kathleen Fisher and Furio Honsell and John C.
Mitchell",
title = "A lambda calculus of objects and method
specialization",
journal = "Nordic Journal of Computing",
year = "1994",
volume = "1",
pages = "3--37",
}
@Article{Fisher:Mitchell95,
title = "The Development of Type Systems for Object-Oriented
Languages",
author = "Kathleen Fisher and John C. Mitchell",
journal = "Theory and Practice of Object Sytems",
pages = "189--220",
year = "1995",
volume = "1",
number = "3",
}
@InProceedings{Fisher:Mitchell:95,
author = "Kathleen Fisher and John C. Mitchell",
title = "A Delegation-based Object Calculus with Subtyping",
booktitle = "Fundamentals of Computation Theory (FCT'95)",
series = "Lecture Notes in Computer Science",
volume = "965",
pages = "42--61",
year = "1995",
publisher = {Springer},
}
@Article{Fisher:Mitchell:98,
author = "Kathleen Fisher and John C. Mitchell",
title = "On the Relationship Between Classes, Objects and Data
Abstraction",
journal = "Theory and Practice of Object Systems",
year = "1998",
volume = "4",
number = "1",
pages = "3--25",
}
@InProceedings{Floyd:67,
author = "Robert W. Floyd",
title = "Assigning Meanings to Programs",
booktitle = "Proceedings of Mathematical Aspects of Computer Science",
month = apr,
year = "1967",
pages = "19--32",
editor = "Jacob T. Schwartz",
volume = "19",
series = "Proceedings of Symposia in Applied Mathematics",
publisher = "American Mathematical Society",
}
@InProceedings{Freyd:91,
author = "Peter J. Freyd",
title = "Algebraically Complete Categories",
editor = "A. Carboni and M. C. Pedicchio and G. Rosolini",
booktitle = "Proceedings of 1990 Como Category Theory Conference",
series = "Lecture Notes in Mathematics",
volume = "1488",
pages = "95--104",
publisher = "Springer",
year = "1991",
}
@Article{Freyd:Rosolini:Mulry:Scott:92,
author = "Peter Freyd and Giuseppe Rosolini and Philip Mulry and
Dana Scott",
title = "Extensional {PERs}",
journal = "Information and Computation",
volume = "98",
number = "2",
special = "Selected Papers from 5th Ann.\ IEEE Symp.\ on Logic in
Computer Science, LICS'90, Philadelphia, PA, USA, 4--7
June 1990",
pages = "211--227",
year = "1992",
}
@Book{GangOfFourBook,
author = "Erich Gamma and Richard Helm and Ralph Johnson and
John Vlissides",
title = "Design Patterns: Elements of Reusable Object-Oriented
Software",
publisher = "Addison Wesley",
year = "1995",
}
@Article{Gapeyev:Levin:Pierce:00,
author = "Vladimir Gapeyev and Michael Y. Levin and Benjamin C.
Pierce",
title = "Recursive subtyping revealed (functional pearl)",
journal = "ACM SIG{\-}PLAN Notices",
volume = "35",
number = "9",
pages = "221--231",
month = sep,
year = "2000",
url = "http://www.acm.org/pubs/citations/proceedings/fp/351240/p221-gapeyev/",
}
@InCollection{Abadi:Leino:04,
author = {Mart{\'\i}n Abadi and K.~R.~M.~Leino},
title = {A Logic of Object-Oriented Programs},
booktitle = {Verification: Theory and Practice. Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday
},
pages = {11--41},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volumne = {2772},
year = {2004},
editor = {Nachum Dershowitz},
}
@Book{Girard:Lafont:Taylor:89,
author = "Jean-Yves Girard and Yves Lafont and Paul Taylor",
title = "Proofs and Types",
publisher = "Cambridge University Press",
series = "Cambridge Tracts in Theoretical Computer Science",
year = "1989",
volume = "7",
}
@Misc{Glimming:05,
author = {Johan Glimming},
title = {\emph{Dialgebraic Semantics of Typed Object Calculi}},
year = 2005,
month = {May},
howpublished = {Licentiate thesis, Stockholm University}
}
@inproceedings{Glimming:Ghani:04,
author = {Johan Glimming and Neil Ghani},
title = {Difunctorial Semantics of Object Calculus},
booktitle = {Proceedings {WOOD} '04: Workshop on Object-Oriented Developments},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
year = 2004,
note = {To appear},
}
@InProceedings{Goerdt:88,
title = "Hoare Calculi for Higher-Type Control Structures and
Their Completeness in the Sense of~{Cook}",
author = "Andreas Goerdt",
booktitle = "Mathematical Foundations of Computer Science 1988",
editor = "Michael P. Chytil and Ladislav Janiga and V{\'a}clav
Koubek",
month = sep,
year = "1988",
series = "Lecture Notes in Computer Science",
volume = "324",
publisher = "Springer",
pages = "329--338",
}
@InCollection{Gordon:98,
author = {Andrew~D.~Gordon},
title = {Operational equivalences for untyped and polymorphic object calculi},
booktitle = {\cite{Gordon:Pitts:98}},
pages = {9--54},
year = {1998},
}
@inproceedings{Gordon:Hankin:00,
author = {Andrew D. Gordon and Paul D. Hankin},
title = {A Concurrent Object Calculus: Reduction and Typing},
booktitle = {Proceedings {HLCL}'98},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
volume = {16},
issue = {3},
editor = {Uwe Nestmann and Benjamin C. Pierce},
year = {2000}
}
@InProceedings{Gordon:Hankin:Lassen:97,
author = "Andrew D. Gordon and Paul D. Hankin and S{\o}ren. B. Lassen",
title = "Compilation and Equivalence of Imperative Objects",
booktitle = "Proceedings of FST+TCS'97",
series = "Lecture Notes in Computer Science",
pages = {74--87},
volume = {1346},
month = dec,
year = "1997",
}
@book{Gordon:Pitts:98,
editor = {Andrew D. Gordon and Andrew M. Pitts},
title = {Higher Order Operational Techniques in Semantics},
publisher = {Cambridge University Press},
series = {Publications of the Newton Institute},
year = 1998,
}
@InProceedings{Gordon:Rees:96,
author = {Andrew~D.~Gordon and Gareth~D.~Rees},
title = {Bisimilarity for a First-Order Calculus of Objects with Subtyping},
booktitle = {Conference Record of the 23rd Symposium on Principles of Programming Languages},
pages = {386--395},
year = {1996},
month = jan,
}
@Book{Gosling:Joy:Steele:Bracha:04,
author = {James Gosling and Bill Joy and Guy Steele and Gilad Bracha},
title = {The Java Language Specification},
publisher = {Addison-Wesley},
year = {2004},
edition = {Third},
}
@InProceedings{Goubault-Larrecq:Lasota:Nowak:02,
author = "Jean {Goubault-Larrecq} and Slawomir Lasota and David
Nowak",
title = "Logical Relations for Monadic Types",
booktitle = "Proc.\ 16th Int.\ Workshop Computer Science Logic (CSL
2002)",
volume = "2471",
pages = "553--568",
series = "Lecture Notes in Computer Science",
year = "2002",
publisher = "Springer",
}
@InProceedings{Goubault-Larrecq:Lasota:Nowak:Zhang:04,
author = "Jean {Goubault-Larrecq} and Slawomir Lasota and David Nowak and
Yu Zhang",
title = "Complete Lax Logical Relations for Cryptographic
Lambda-Calculi",
booktitle = "Proc.\ 18th Int.\ Workshop Computer Science Logic (CSL
2004)",
volume = "3210",
series = "Lecture Notes in Computer Science",
pages = "400--414",
year = "2004",
publisher = "Springer",
}
@InProceedings{Halpern:84,
author = "Joseph Y. Halpern",
title = "A Good {H}oare Axiom System for an {A}lgol-Like
Language",
booktitle = "Conference Record of the Eleventh Annual {ACM}
Symposium on Principles of Programming Languages",
publisher = "ACM Press",
month = jan,
year = "1984",
pages = "262--271",
}
@Article{Hasegawa:94,
title = "Categorical data types in parametric polymorphism",
author = "Ryu Hasegawa",
pages = "71--109",
journal = "Mathematical Structures in Computer Science",
month = mar,
year = "1994",
volume = "4",
number = "1",
}
@Book{Haskell98,
editor = {Simon {Peyton Jones}},
title = {Haskell 98 Language and Libraries. The Revised Report},
publisher = {Cambridge University Press},
year = {2003},
OPTmonth = {April},
}
@InProceedings{Hensel:Huismann:Jacobs:Tews:98,
title = "Reasoning about Classes in Object-Oriented Languages:
Logical Models and Tools",
author = "Ulrich Hensel and Marieke Huisman and Bart Jacobs and
Hendrik Tews",
booktitle = "Programming Languages and Systems---{ESOP}'98, 7th
European Symposium on Programming",
editor = "Chris Hankin",
month = mar,
year = "1998",
series = "Lecture Notes in Computer Science",
volume = "1381",
pages = "105--121",
publisher = {Springer},
}
@Article{Hoare:69,
author = "C. A. R. Hoare",
title = "{An Axiomatic Basis of Computer Programming}",
journal = "Communications of the ACM",
year = "1969",
volume = "12",
pages = "576--580",
publisher = "ACM Press",
}
@Article{Hofmann:Pierce:94,
author = "Martin Hofmann and Benjamin Pierce",
title = "A Unifying Type-Theoretic Framework for Objects",
journal = "Journal of Functional Programming",
volume = "5",
number = "4",
pages = "593--635",
month = oct,
year = "1995",
}
@Article{Hofmann:Pierce:95,
author = "Martin Hofmann and Benjamin C. Pierce",
title = "A Unifying Type-Theoretic Framework for Objects",
journal = "Journal of Functional Programming",
month = oct,
year = "1995",
volume = "5",
number = "4",
pages = "593--635",
}
@Article{Hofmann:Pierce:96,
author = {Martin Hofmann and Benjamin Pierce},
title = {Positive Subtyping},
journal = {Information and Computation},
year = {1996},
volume = {126},
number = {1},
pages = {11--33},
}
@Misc{Hofmann:Tang:02,
author = {Francis Tang and Martin Hofmann},
title = {Generation of Verification Conditions for {Abadi} and {Leino}'s Logic of Objects},
howpublished = {Presented at 9th International Workshop on Foundations of Object-Oriented Languages},
month = jan,
year = {2002},
}
@InProceedings{Berger:Honda:Yoshida:05,
author = "Martin Berger and Kohei Honda and Nobuko Yoshida",
title = "A Logical Analysis of Aliasing in Imperative
Higher-Order Functions",
booktitle = "Proceedings of the 10th {ACM} {SIGPLAN} International
Conference on Functional Programming ({ICFP} '05)",
publisher = "ACM Press",
year = "2005",
notes = "To appear",
}
@InProceedings{Honda:Yoshida:Berger:05,
author = {Kohei Honda and Nobuko Yoshida and Martin Berger},
title = {An Observationally Complete Program Logic for Imperative Higher-Order Functions},
booktitle = {{LICS'05}},
pages = {270--279},
year = 2005,
}
@Article{Honda:04,
author = "Kohei Honda",
title = "From process logic to program logic",
journal = "ACM SIG{\-}PLAN Notices",
volume = "39",
number = "9",
pages = "163--174",
month = sep,
year = "2004",
}
@Article{Honsell:Pravato:Rocca:98,
title = "{Structured Operational Semantics} of a fragment of
the language {Scheme}",
author = "Furio Honsell and Alberto Pravato and Simona Ronchi
Della Rocca",
pages = "335--365",
journal = "Journal of Functional Programming",
month = jul,
year = "1998",
volume = "8",
number = "4",
}
@InProceedings{Igarashi:Pierce:00,
author = {Atsushi Igarashi and Benjamin C. Pierce},
title = {On inner Classes},
booktitle = {Proceedings of the European Conference on Object-Oriented Programming},
pages = {129--153},
year = {2000},
volume = {1850},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
}
@Article{Ishtiaq:OHearn:01,
author = "Samin S. Ishtiaq and Peter W. O'Hearn",
title = "{BI} as an Assertion Language for Mutable Data
Structures",
journal = "ACM SIG{\-}PLAN Notices",
volume = "36",
number = "3",
pages = "14--26",
month = mar,
year = "2001",
}
@inproceedings{Jacobs:00,
author = {Bart Jacobs},
title = {Subtypes and bounded quantification from a fibred perspective},
booktitle = {Electronic Notes in Theoretical Computer Science},
volume = {1},
editor = {S. Brookes, M. Main, A. Melton and M. Mislove},
year = {2000},
publisher = {Elsevier},
}
@InCollection{Jacobs:96,
author = "Bart P. F. Jacobs",
title = "Objects and classes, coalgebraically",
editor = "B. Freitag and C. B. Jones and C. Lengauer and H. J.
Schek",
booktitle = "Object-Orientation with Parallelism and Persistence",
pages = "83--103",
publisher = "Kluwer Academic Publishers",
year = "1996",
url = "http://www.cwi.nl/pub/CWIreports/AP/CS-R9536.ps.Z",
}
@InProceedings{Jacobs:Poll:01,
author = "Bart Jacobs and Erik Poll",
title = "A Logic for the {Java} Modeling Language {JML}",
series = "Lecture Notes in Computer Science",
volume = "2029",
pages = "284--299",
year = "2001",
booktitle = "Fundamental Approaches to Software Engineering
(FASE'2001)",
publisher = "Springer",
}
@Article{Jacobs:Poll:03,
author = "Bart Jacobs and Erik Poll",
title = "Coalgebras and monads in the semantics of {Java}",
journal = "Theoretical Computer Science",
volume = "291",
number = "3",
pages = "329--349",
year = "2003",
}
@Article{Jacobs:Rutten:97,
author = "Bart Jacobs and Jan Rutten",
title = "A Tutorial on (Co)Algebras and (Co)Induction",
journal = "Bulletin of the European Association for Theoretical
Computer Science",
volume = "62",
pages = "222--259",
month = jun,
year = "1997",
}
@inproceedings{Jeffrey:Rathke:02,
author = {Alan Jeffrey and Julian Rathke},
year = {2002},
title = {A fully abstract may testing semantics for concurrent objects},
booktitle = {Proceedings $17^{th}$ Annual Symposium on Logic in Computer Science},
publisher = {IEEE Computer Society Press},
pages = {101--112}
}
@inproceedings{Jeffrey:Rathke:99,
author = {Alan Jeffrey and Julian Rathke},
title = {Towards a theory of bisimulation for local names},
booktitle = {Proc. LICS'99, 14th Annual Symposium on Logic in Computer Science},
year = {1999},
publisher = {IEEE Computer Society Press},
pages = {56--66},
}
@InCollection{Kamin:Reddy:94,
author = "Samuel N. Kamin and Uday S. Reddy",
title = "Two Semantic Models of Object-Oriented Languages",
booktitle = "Theoretical Aspects of Object-Oriented Programming:
Types, Semantics, and Language Design",
editor = "Carl A. Gunter and John C. Mitchell",
publisher = "MIT Press",
pages = "464--495",
year = "1994",
}
@Book{Kernighan:Ritchie:88,
author = {Brian Kernighan and Dennis Ritchie},
title = {The {C} Programming Language},
publisher = {Prentice-Hall},
year = {1988},
edition = {Second},
}
@InProceedings{Kleist:Sangiorgi:98,
author = "Josva Kleist and Davide Sangiorgi",
title = "Imperative Objects and Mobile Processes",
pages = "285--303",
booktitle = "Programming Concepts and Methods",
year = "1998",
editor = "David Gries and Willem-Paul {de Roever}",
}
@article{Kleymann:99,
author = "Thomas Kleymann",
title = "Hoare Logic and Auxiliary Variables",
journal = "Formal Aspects of Computing",
volume = "11",
number = "5",
pages = "541--566",
year = "1999",
month = dec,
}
@InProceedings{Laeufer:95,
author = "L{\"{a}}ufer, K.",
title = "A Framework for Higher-Order Functions in {C}++",
booktitle = "Proceedings of Conference on Object-Oriented Technologies",
year = 1995,
address = "Monterey, CA",
month = jun,
pages = "103--116",
}
@InProceedings{Laird:02,
author = {James Laird},
title = {A Categorical Semantics of Higher-Order Store},
booktitle = {Proceedings of the 9th Conference on Category Theory and Computer Science, CTCS '02},
pages = {1--18},
year = {2003},
editor = {Rick Blute and Peter Selinger},
volume = {69},
series = {Electronic notes in Theoretical Computer Science},
publisher = {Elsevier},
}
@Article{Landin:64,
author = "Peter J. Landin",
title = "The Mechanical Evaluation of Expressions",
journal = "Computer Journal",
volume = "6",
number = "4",
month = jan,
year = "1964",
pages = "308--320",
}
@InProceedings{Leino:98,
title = "Recursive Object Types in a Logic of Object-Oriented
Programs",
author = "K. Rustan M. Leino",
booktitle = "7th European Symposium on Programming",
editor = "Chris Hankin",
month = mar,
year = "1998",
series = "Lecture Notes in Computer Science",
publisher = {Springer},
volume = "1381",
pages = "170--184",
}
@InProceedings{Levy:02,
author = "Paul Blain Levy",
title = "Possible World Semantics for General Storage in
Call-By-Value",
booktitle = "CSL: 16th Workshop on Computer Science Logic",
series = "Lecture Notes in Computer Science",
volume = "2471",
editor = "Julian Bradfield",
publisher = "Springer",
year = "2002",
}
@Book{Levy:04,
author = {Paul Blain Levy},
title = {Call-By-Push-Value. A Functional/Imperative Synthesis},
publisher = {Kluwer},
year = {2004},
volume = {2},
series = {Semantic Structures in Computation},
}
@Article{Liang:Bracha:98,
author = "Sheng Liang and Gilad Bracha",
title = "Dynamic Class Loading in the {Java Virtual Machine}",
pages = "36--44",
booktitle = "Proceedings of the 13th Conference on Object-Oriented
Programming, Systems, Languages, and Applications",
month = oct,
journal = "ACM SIGPLAN Notices",
volume = "33",
number = "10",
publisher = "ACM Press",
year = "1998",
}
@Article{Liskov:Wing:94,
author = "Barbara H. Liskov and Jeannette M. Wing",
title = "A Behavioral Notion of Subtyping",
journal = "ACM Transactions on Programming Languages and
Systems",
volume = "16",
number = "6",
pages = "1811--1841",
month = nov,
year = "1994",
}
@PhdThesis{Longley:95,
author = "John Longley",
title = "Realizability toposes and language semantics",
school = "University of Edinburgh",
year = "1995",
}
@Article{Longo:Moggi:91,
author = "Giuseppe Longo and Eugenio Moggi",
title = "Constructive Natural Deduction and its `$\omega$-set'
Interpretation",
journal = "Mathematical Structures in Computer Science",
pages = "215--254",
volume = "1",
number = "2",
month = jul,
year = "1991",
}
@InProceedings{Ma:Reynolds:92,
author = "QingMing Ma and John C. Reynolds",
title = "Types, Abstraction, and Parametric Polymorphism, Part
2",
booktitle = "Proceedings 7th International Conference on Mathematical Foundations of Programming Semantics",
editor = "Stephen Brookes and Michael Main and Austin Melton and
Michael Mislove and David A. Schmidt",
series = "Lecture Notes in Computer Science",
volume = "598",
publisher = "Springer",
year = "1992",
pages = "1--40",
}
@Book{MacLane:97,
author = {Saunders {Mac Lane}},
title = {Categories for the Working Mathematician},
series = {Graduate Texts in Mathematics},
volume = {5},
publisher = {Springer},
year = {1997},
}
@Article{MacQueen:Plotkin:Sethi:86,
author = "David B. MacQueen and Gordon D. Plotkin and Ravi
Sethi",
title = "An Ideal Model for Recursive Polymorphic Types",
journal = "Information and Control",
month = oct,
volume = "71",
number = "1--2",
year = "1986",
pages = "95--130",
}
@InProceedings{Meyer:Sieber:88,
author = "Albert R. Meyer and K. Sieber",
title = "Towards Fully Abstract Semantics for Local Variables:
Preliminary Report",
pages = "191--203",
booktitle = "Conference Record of the Fifteenth Annual {ACM}
Symposium on Principles of Programming Languages",
year = "1988",
publisher = "ACM Press",
month = jan,
}
@Article{Milner:78,
author = "Robin Milner",
journal = "Journal of Computer and System Science",
pages = "348--375",
title = "A Theory of Type Polymorphism in Programming
Languages",
volume = "17",
number = "3",
year = "1978",
}
@InProceedings{Mitchell:90,
author = "John C. Mitchell",
title = "Toward a Typed Foundation for Method Specialization
and Inheritance",
booktitle = "Conference Record of the 17th Annual {ACM}
Symposium on Principles of Programming
Languages",
publisher = {ACM Press},
year = "1990",
pages = "109--124",
month = jan,
}
@InCollection{Mitchell:91,
author = "John C. Mitchell",
title = "On the Equivalence of Data Representations",
editor = "V. Lifschitz",
booktitle = "Artificial Intelligence and Mathematical Theory of
Computation: Papers in Honor of {John McCarthy}",
publisher = "Academic Press",
pages = "305--330",
year = "1991",
}
@Book{Mitchell:96,
author = "John C. Mitchell",
title = "Foundations for Programming Languages",
publisher = "MIT Press",
year = "1996",
}
@Article{Mitchell:Moggi:91,
author = "John C. Mitchell and Eugenio Moggi",
title = "{K}ripke-Style Models for Typed Lambda Calculus",
journal = "Annals of Pure and Applied Logic",
volume = "51",
number = "1--2",
pages = "99--124",
year = "1991",
}
@Article{Mitchell:Plotkin:88,
author = "John C. Mitchell and Gordon D. Plotkin",
title = "Abstract Types Have Existential Type",
journal = "ACM Transactions on Programming Languages and
Systems",
volume = "10",
number = "3",
pages = "470--502",
month = jul,
year = "1988",
}
@InProceedings{Mitchell:Scedrov:93,
author = "John C. Mitchell and Andre Scedrov",
title = "Notes on Sconing and Relators",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "702",
pages = "352--378",
year = "1993",
booktitle = "Computer Science Logic '92, Selected Papers",
editor = {Egon B{\"o}rger and
Gerhard J{\"a}ger and
Hans Kleine B{\"u}ning and
Simone Martini and
Michael M. Richter},
}
@InProceedings{Mitchell:Viswanathan:96,
title = "Effective Models of Polymorphism, Subtyping and
Recursion (Extended Abstract)",
author = "John C. Mitchell and Ramesh Viswanathan",
editor = "Friedhelm {Meyer auf der Heide} and Burkhard Monien",
booktitle = "23rd International Colloquium on Automata, Languages and Programming",
month = jul,
year = "1996",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
volume = "1099",
pages = "170--181",
}
@Article{Moggi:Sabry:04,
author = "Eugenio Moggi and Amr Sabry",
title = "An Abstract Monadic Semantics for Value Recursion",
journal = "Theoretical Informatics and Applications",
volume = "38",
number = "4",
special = "Selected Papers from 5th Int.\ Wksh.\ on Fixed Points
in Comp.\ Sci., FICS 2003, Warsaw, Poland, 12--13 Apr.\
2003",
pages = "375--400",
year = "2004",
}
@Misc{Niehren:Schwinghammer:Smolka:Futures,
author = {Joachim Niehren and Jan Schwinghammer and Gert Smolka},
title = {Concurrent Computation in a Lambda Calculus with Futures},
year = {2003},
howpublished = {Draft},
}
@inproceedings{Nipkow:Oheimb:02,
author={David von Oheimb and Tobias Nipkow},
title={Hoare Logic for {NanoJava}: Auxiliary Variables, Side Effects and
Virtual Methods Revisited},
booktitle={Formal Methods Europe (FME 2002)},
editor={L.-H. Eriksson and P. Lindsay},
publisher={Springer},
series={LNCS},
volume=2391,
pages={89-105},
year={2002},
}
@Article{OHearn:03,
author = {Peter W. O'Hearn},
title = {On Bunched Typing},
journal = {Journal of Functional Programming},
year = {2003},
pages = {747--796},
volume = {13},
number = "4",
}
@Article{OHearn:98,
author = {Peter W. O'Hearn},
title = {Polymorphism, Objects and Abstract Types},
journal = {{SIGACT} News},
year = {1998},
volume = {29},
number = {4},
pages = {39--50},
month = dec,
}
@Article{OHearn:Pym:99,
author = {Peter W. O'Hearn and David J. Pym},
title = {The Logic of Bunched Implications},
journal = {Bulletin of Symbolic Logic},
year = {1999},
volume = {5},
number = {2},
pages = {215--244},
month = jun,
}
@Article{OHearn:Reddy:99,
author = {Peter W. O'Hearn and Uday S. Reddy},
title = {Objects, interference and the Yoneda embedding},
journal = {Theoretical Computer Science},
year = {1999},
volume = {228},
number = {1--2},
pages = {253--282},
}
@InProceedings{OHearn:Reynolds:Yang:01,
author = {Peter W. O'Hearn and John C. Reynolds and Hongseok Yang},
title = {Local Reasoning about Programs that Alter Data Structures},
booktitle = {Proceedings Computer Science Logic (CSL'01)},
pages = {1--18},
year = {2001},
editor = {L. Fribourg},
volume = {2142},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
}
@Article{OHearn:Tennent:95,
title = "Parametricity and Local Variables",
author = "Peter W. O'Hearn and Robert D. Tennent",
pages = "658--709",
journal = "Journal of the ACM",
month = may,
year = "1995",
volume = "42",
number = "3",
}
@Book{OHearn:Tennent:97,
editor = "Peter W. O'Hearn and Robert D. Tennent",
title = "{{A}lgol-Like Languages, Vols {I} and {II}}",
publisher = "Birkhauser",
year = "1997",
series = "Progress in Theoretical Computer Science",
}
@Article{Ohori:Buneman:89,
key = "Ohori \& Buneman",
author = "Atsushi Ohori and Peter Buneman",
title = "Static Type Inference for Parametric Classes",
journal = "ACM SIGPLAN Notices",
volume = "24",
number = "10",
month = oct,
year = "1989",
pages = "445--456",
editor = "Norman Meyerowitz",
note = "OOPSLA '89 Conference Proceedings",
}
@PhdThesis{Oles:82,
title = "A Category-theoretic approach to the semantics of
programming languages",
author = "Frank Joseph Oles",
year = "1982",
school = "Syracuse University",
}
@Article{Palsberg:95,
title = "Efficient Inference of Object Types",
author = "Jens Palsberg",
pages = "198--209",
journal = "Information and Computation",
month = dec,
year = "1995",
volume = "123",
number = "2",
}
@Book{Paulson:87,
author = "Larry C. Paulson",
title = "Logic and Computation : Interactive proof with
Cambridge {LCF}",
series = "Cambridge Tracts in Theoretical Computer Science",
volume = "2",
year = "1987",
publisher = "Cambridge University Press",
}
@TechReport{Phoa:92,
author = "Wesley Phoa",
title = "An Introduction to Fibrations, Topos Theory, the
Effective Topos and Modest Sets",
number = "ECS-LFCS-92-208",
institution = "Department of Computer Science, University of
Edinburgh",
year = "1992",
}
@Book{Pierce:02,
author = "Benjamin C. Pierce",
title = "Types and Programming Languages",
publisher = "The MIT Press",
year = "2002",
}
@Book{Pierce:91,
author = "Benjamin C. Pierce",
title = "Basic Category Theory for Computer Scientists",
publisher = "MIT Press",
year = "1991",
}
@Article{Pierce:Turner:94,
author = "Benjamin C. Pierce and David N. Turner",
title = "Simple Type-Theoretic Foundations for Object-Oriented
Programming",
journal = "Journal of Functional Programming",
volume = "4",
number = "2",
pages = "207--247",
year = "1994",
}
@Article{Pierik:deBoer:05,
author = {Cees Pierik and Frank S. de Boer},
title = {A Proof Outline Logic for Object-Oriented Programming},
journal = {Theoretical Computer Science},
year = {2005},
note = {To appear},
}
@InProceedings{Pitts:87,
author = "Andrew M. Pitts",
title = "Polymorphism is Set Theoretic, Constructively",
booktitle = "Category Theory and Computer Science",
editor = "D. H. Pitt and A. Poign\'{e} and David E. Rydeheard",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
volume = "283",
year = "1987",
}
@ARTICLE{pitts:relational,
AUTHOR={Andrew M. Pitts},
TITLE={Relational Properties of Domains},
JOURNAL={Information and Computation},
VOLUME=127,
YEAR=1996,
PAGES={66--90},
}
@InProceedings{Pitts:Stark:93,
author = "Andrew M. Pitts and Ian D. B. Stark",
title = "Observable Properties of Higher Order Functions That
Dynamically Create Local Names, or: What's new?",
booktitle = "Proceedings 18th International Symposium on Mathematical Foundations of Computer Science",
editor = "Andrzej M. Borzyszkowski and Stefan Sokolowski",
series = "Lecture Notes in Computer Science",
volume = "711",
publisher = "Springer",
year = "1993",
pages = "122--141",
}
@InProceedings{pitts-stark:state,
author = "Andrew Pitts and Ian Stark",
title = "Operational Reasoning for Functions with Local State",
booktitle = "HOOTS",
year = "1998",
}
@InProceedings{chin+:popl08,
author = {Wei-Ngan Chin and Cristina David and Huu Hai Nguyen and Shengchao Qin},
title = {Enhancing Modular {OO} Verification with Separation Logic},
booktitle = "POPL",
year = 2008,
}
@Unpublished{Plotkin:83,
author = {Gordon D. Plotkin},
title = {Domain Theory},
note = "Pisa notes",
year = {1983},
}
@Article{Plotkin:Smyth:82,
author = "Michael B. Smyth and Gordon D. Plotkin",
title = "The Category-theoretic Solution of Recursive Domain
Equations",
journal = "SIAM J. Comput.",
volume = "11",
number = "4",
pages = "761--783",
year = "1982",
}
@InProceedings{Poetzsch-Heffter:Mueller:98,
author = "Arnd Poetzsch-Heffter and Peter M{\"u}ller",
title = "Logical Foundations for Typed Object-Oriented
Languages",
editor = "David Gries and Willem-Paul {De~Roever}",
booktitle = "Proceedings {IFIP} Working Conference on Programming
Concepts and Methods",
year = "1998",
publisher = "Chapman \& Hall",
}
@InProceedings{Poetzsch-Heffter:Mueller:99,
key = "Poetzsch-Heffter \& M{\"u}ller",
author = "Arnd Poetzsch-Heffter and Peter M{\"u}ller",
title = "A Programming Logic for Sequential {J}ava",
booktitle = "European Symposium on Programming",
editor = "S. D. Swierstra",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
volume = "1576",
pages = "162--176",
year = "1999",
}
@Article{Pym:OHearn:Yang:04,
author = "David J. Pym and Peter W. O'Hearn and Hongseok
Yang",
title = "Possible worlds and resources: the semantics of {BI}",
journal = "Theoretical Computer Science",
volume = "315",
number = "1",
pages = "257--305",
day = "5",
month = may,
year = "2004",
}
@Article{Reddy:02,
author = {Uday S.~Reddy},
title = {Objects and classes in Algol-like languages},
journal = {Information and Computation},
year = {2002},
volume = {172},
number = {1},
pages = {63--97},
month = {January},
}
@Article{Reddy:96,
author = "Uday S. Reddy",
title = "Global State Considered Unnecessary: An Introduction
to Object-Based Semantics",
journal = "{LISP} and Symbolic Computation",
volume = "9",
number = "1",
pages = "7--76",
month = feb,
year = "1996",
}
@Misc{Reddy:98,
author = {Uday S. Reddy},
title = {Objects and Classes in {Algol}-like Languages},
year = {1998},
note = {Presented at {FOOL} 5 workshop},
}
@Article{Reddy:Yang:04,
author = {Uday S. Reddy and Hongseok Yang},
title = {Correctness of Data Representations Involving Heap
Data Structures},
journal = {Science of Computer Programming},
year = {2004},
volume = {50},
number = {1--3},
pages = {129--160},
month = {March},
}
@Article{Remy:Vouillon:98,
author = "Didier R{\'e}my and J{\'e}r{\^o}me Vouillon",
title = "Objective {ML}:
An effective object-oriented extension to {ML}",
journal = "Theory And Practice of Object Systems",
year = 1998,
volume = "4",
number = "1",
pages = "27--50",
}
@InProceedings{Reus:02,
author = {Bernhard Reus},
title = {Class-based versus Object-based: A Denotational Comparison},
booktitle = {Proceedings of 9th International Conference on Algebraic Methodology And Software
Technology},
series = "Lecture Notes in Computer Science",
publisher = "Springer",
editor = {H{\'}el{\`}ene Kirchner and Christophe Ringeissen},
volume = {2422},
pages = {473--488},
year = {2002},
}
@INPROCEEDINGS{Reus:03,
author = {B.~Reus},
title = {Modular Semantics and Logics of Classes},
booktitle = "Computer Science Logic",
pages = "456--469",
editor = "Matthias Baatz and Johann A.~Makowsky",
publisher = "Springer",
Series = "Lecture Notes in Computer Science",
volume = "2803",
year = "2003"
}
@Unpublished{Reus:99,
author = {Bernhard Reus},
title = {Realizability Models for Type Theories},
note = {Draft of a Tutorial for the {R}ealizability {W}orkshop'99 in {T}rento},
month = nov,
year = {2000},
}
@TechReport{Reus:Schwinghammer:04,
author = {Bernhard Reus and Jan Schwinghammer},
title = {Denotational Semantics for {Abadi} and {Leino}'s Logic of Objects},
institution = {Informatics, University of Sussex},
year = {2004},
number = {2004:03},
}
@InProceedings{Reus:Schwinghammer:05,
author = {Bernhard Reus and Jan Schwinghammer},
title = {Denotational Semantics for {Abadi} and {Leino}'s Logic of Objects},
booktitle = {Proceedings of the European Symposium on Programming},
year = {2005},
pages = {264--279},
editor = {Mooly Sagiv},
series = {Lecture Notes in Computer Science},
volume = {3444},
publisher = {Springer},
}
@InProceedings{Reus:Streicher:02,
author = {Bernhard Reus and Thomas Streicher},
title = {Semantics and Logic of Object Calculi},
booktitle = {Proceedings of 17th Annual IEEE Symposium Logic in Computer Science},
publisher = {IEEE Computer Society Press},
year = {2002},
pages = {113--124},
}
@Article{Reus:Streicher:04,
author = {Bernhard Reus and Thomas Streicher},
title = {Semantics and Logic of Object Calculi},
journal = {Theoretical Computer Science},
year = {2004},
volume = {316},
publisher = "Elsevier",
pages = {191--213},
}
@INPROCEEDINGS{Reus:Wirsing:Hennicker:01,
Author = "B.~Reus and M.~Wirsing and R.~Hennicker",
Title = "{A Hoare-Calculus for Verifying Java Realizations of OCL-Constrained Design Models}",
Booktitle = "FASE 2001",
Year = 2001,
Editor = "Heinrich Hussmann",
Publisher = "Springer",
Volume = 2029,
Pages = "300--317",
Series = "Lecture Notes in Computer Science",
}
@incollection{Reynolds:02a,
author = "Reynolds, John C.",
title = "What do Types Mean? --- {From} Intrinsic to Extrinsic Semantics",
booktitle = "Essays on Programming Methodology",
editor = "Annabelle McIver and Carroll Morgan",
publisher = "Springer",
year = "2002",
}
@InProceedings{Reynolds:02,
author = "John C. Reynolds",
title = "Separation Logic: {A} Logic for Shared Mutable Data
Structures",
pages = "55--74",
booktitle = "LICS'02",
year = "2002"
}
@InProceedings{hobor+:esop08,
author = {Aquinas Hobor and Andrew Appel and Francesco {Zappa Nardelli}},
title = {Oracle Semantics for Concurrent Separation Logic},
booktitle = {ESOP},
year = {2008},
pages = {353--367},
}
@InProceedings{stovring+:popl07,
author = {Kristian St\o{}vring and Soren Lassen},
title = {A Complete, Co-Inductive Syntactic Theory of Sequential Control and State},
booktitle = {POPL},
year = {2007},
}
@InProceedings{lassen+:lics08,
author = {Soren B. Lassen and Paul Blain Levy},
title = {Typed Normal Form Bisimulation for Parametric Polymorphism},
booktitle = {LICS},
year = {2008},
}
@inproceedings{meyer-sieber-1988,
author = "Albert R. Meyer and Kurt Sieber",
title = "Towards fully abstract semantics for local variables",
booktitle = {POPL},
year = 1988,
}
@InProceedings{pottier:lics08,
author = {Fran\c{c}ois Pottier},
title = {Hiding local state in direct style: a higher-order anti-frame rule},
booktitle = {LICS},
year = {2008},
}
@InProceedings{hobor+:popl10,
author = {Aquinas Hobor and Robert Dockins and Andrew Appel},
title = {A Theory of Indirection via Approximation},
booktitle = {POPL},
year = {2010},
}
@InProceedings{Dockins+:aplas09,
author={Robert Dockins and Aquinas Hobor and Andrew W. Appel},
title={A Fresh Look at Separation Algebras and Share Accounting},
booktitle={APLAS},
year={2009},
pages={161--177},
}
@InProceedings{Balabonski+:flops14,
author={Thibaut Balabonski and Fran\c{c}ois Pottier and Jonathan Protzenko},
title={Type Soundness and Race Freedom for {M}ezzo},
booktitle={FLOPS},
year={2014},
}
@Article{Pottier:jfp13,
author={Fran\c{c}ois Pottier},
title={Syntactic soundness proof of a type-and-capability system with hidden state},
journal={JFP},
volume={23},
number={1},
pages={38--144},
year={2013},
}
@Unpublished{pottier:generalized,
author = {Fran\c{c}ois Pottier},
title = {Generalizing the higher-order frame and anti-frame rules},
note = {Unpublished},
year = {2009},
mon = jul,
}
@inproceedings{pilkiewicz+:monotonic,
author = {Alexandre Pilkiewicz and Fran\c{c}ois Pottier},
title = {The Essence of Monotonic State},
booktitle = {TLDI},
year = 2011,
}
@InProceedings{schwinghammer+:antiframe,
author = {Jan Schwinghammer and Hongseok Yang and Lars Birkedal and Fran\c{c}ois Pottier and Bernhard Reus},
title = {A Semantic Foundation for Hidden State},
booktitle = {FOSSACS},
year = 2010,
}
@InProceedings{chargueraud+:icfp08,
author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
title = {Functional translation of a calculus of capabilities},
booktitle = {ICFP},
year = {2008},
}
@InProceedings{benton+:tldi09,
author = {Nick Benton and Nicolas Tabareau},
title = {Compiling functional types to relational specifications for low level imperative code},
booktitle = {TLDI},
year = {2009},
}
@InProceedings{benton+:icfp09,
author = {Nick Benton and Chung-Kil Hur},
title = {Biorthogonality, Step-Indexing and Compiler Correctness},
booktitle = {ICFP},
year = 2009}
@InProceedings{benton-tabareau-tldi2009,
author = {Nick Benton and Nicolas Tabareau},
title = {Compiling Functional Types to Relational Specifications for Low Level Imperative Code},
booktitle = {TLDI},
year = {2009},
}
@article{DBLP:journals/iandc/AbramskyJM00,
author = {Samson Abramsky and
Radha Jagadeesan and
Pasquale Malacaria},
title = {Full Abstraction for PCF},
journal = {Inf. Comput.},
volume = {163},
number = {2},
year = {2000},
pages = {409-470},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/iandc/HylandO00,
author = {J. M. E. Hyland and
C.-H. Luke Ong},
title = {On Full Abstraction for PCF: I, II, and III},
journal = {Inf. Comput.},
volume = {163},
number = {2},
year = {2000},
pages = {285-408},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@Unpublished{koutavas-lassen,
author = {V. Koutavas and S. Lassen},
title = {Fun with Fully Abstract Operational Game Semantics for General References},
note = {Unpublished},
month = feb,
year = 2008
}
@InProceedings{murawski+:lics11,
author = {Andrzej S. Murawski and Nikos Tzevelekos},
title = {Game semantics for good general references},
booktitle = {LICS},
year = {2011},
}
@inproceedings{laird:icalp07,
author = {James Laird},
title = {A Fully Abstract Trace Semantics for General References},
booktitle = {ICALP},
year = {2007}
}
@inproceedings{DBLP:conf/fossacs/Laird04,
author = {James Laird},
title = {A Game Semantics of Local Names and Good Variables},
booktitle = {Foundations of Software Science and Computation Structures,
7th International Conference, FOSSACS 2004, Held as Part
of the Joint European Conferences on Theory and Practice
of Software, ETAPS 2004, Barcelona, Spain, March 29 - April
2, 2004, Proceedings},
year = {2004},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2987},
pages = {289-303},
ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2987{\&}spage=289},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{lassen+:csl07,
author = {Soren B. Lassen and
Paul Blain Levy},
title = {Typed Normal Form Bisimulation},
booktitle = {CSL},
year = {2007}
}
@inproceedings{DBLP:conf/fossacs/MurawskiT09,
author = {Andrzej S. Murawski and
Nikos Tzevelekos},
title = {Full Abstraction for Reduced ML},
booktitle = {FOSSACS},
year = {2009}
}
@article{DBLP:journals/tcs/MurawskiW08,
author = {Andrzej S. Murawski and
Igor Walukiewicz},
title = {Third-order {Idealized Algol} with iteration is decidable},
journal = {TCS},
volume = {390},
number = {2--3},
year = {2008},
pages = {214--229}
}
@inproceedings{DBLP:conf/icalp/GhicaM00,
author = {Dan R. Ghica and
Guy McCusker},
title = {Reasoning about {Idealized Algol} Using Regular Languages},
booktitle = {ICALP},
year = {2000}
}
@inproceedings{DBLP:conf/galop/Murawski05,
author = {Andrzej S. Murawski},
title = {Functions with local state: from regularity to undecidability},
booktitle = {GALOP},
year = {2005}
}
@inproceedings{DBLP:conf/icalp/MurawskiOW05,
author = {Andrzej S. Murawski and
C.-H. Luke Ong and
Igor Walukiewicz},
title = {{Idealized Algol} with Ground Recursion, and DPDA Equivalence},
booktitle = {ICALP 2005},
year = 2005
}
@article{murawski-rml-badvars,
author = {Andrzej S. Murawski},
title = {Functions with local state: regularity and undecidability},
journal = {TCS},
volume = {338},
number = {1--3},
year = {2005},
pages = {315--349}
}
@inproceedings{DBLP:conf/lics/McCusker96,
author = {Guy McCusker},
title = {Games and Full Abstraction for FPC},
booktitle = {LICS},
year = {1996},
pages = {174-183},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/fossacs/AbramskyJ03,
author = {Samson Abramsky and
Radha Jagadeesan},
title = {A Game Semantics for Generic Polymorphism},
booktitle = {Foundations of Software Science and Computational Structures,
6th International Conference, FOSSACS 2003 Held as Part
of the Joint European Conference on Theory and Practice
of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003,
Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2620},
year = {2003},
pages = {1-22},
ee = {http://link.springer.de/link/service/series/0558/bibs/2620/26200001.htm},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/lics/LongoMS93,
author = {Giuseppe Longo and
Kathleen Milsted and
Sergei Soloviev},
title = {The Genericity Theorem and the Notion of Parametricity in
the Polymorphic lambda-calculus (Extended Abstract)},
booktitle = {LICS},
year = {1993}
}
@inproceedings{DBLP:conf/lics/AbramskyHM98,
author = {Samson Abramsky and
Kohei Honda and
Guy McCusker},
title = {A Fully Abstract Game Semantics for General References},
booktitle = {LICS},
year = {1998},
}
@inproceedings{abramsky-mccusker-lecturenotes,
author = {Samson Abramsky and
Guy McCusker},
title = {Game Semantics},
booktitle = {Proceedings of the 1997 Marktoberdorf Summer School},
year = {1998}
}
@inproceedings{DBLP:conf/lics/Hughes97,
author = {Dominic J. D. Hughes},
title = {Games and Definability for System F},
booktitle = {LICS},
year = {1997}
}
@Unpublished{laird:icalpsubmission,
author = {James Laird},
title = {Game Semantics for Call-by-Value Polymorphism},
note = {Manuscript},
month = {March},
year = 2010
}
@article{DBLP:journals/entcs/AbramskyM96,
author = {Samson Abramsky and
Guy McCusker},
title = {Linearity, Sharing and State: a fully abstract game semantics
for {Idealized Algol} with active expressions},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {3},
year = {1996}
}
@InProceedings{ohearn-reddy-95,
author = {Peter O'Hearn and Uday Reddy},
title = {Objects, Interference, and the {Y}oneda Embedding},
booktitle = {MFPS},
year = 1995}
@InProceedings{pitts:96,
author = {Andrew M. Pitts},
title = {Reasoning about Local Variables with Operationally-Based Logical Relations},
booktitle = {LICS},
year = 1996}
@InProceedings{sumii:csl09,
author = {Eijiro Sumii},
title = {A Complete Characterization of Observational Equivalence in Polymorphic $\lambda$-Calculus with General References},
booktitle = {CSL},
year = 2009}
@inproceedings{sangiorgi+:lics07,
title = {Environmental Bisimulations for Higher-Order Languages},
author = {Davide Sangiorgi and Naoki Kobayashi and Eijiro Sumii},
booktitle = {LICS},
year = 2007,
}
@inproceedings{bohr-birkedal-2006,
author = "Nina Bohr and Lars Birkedal",
title = {Relational reasoning for recursive types and references},
booktitle = {APLAS},
year = 2006,
}
@PhdThesis{bohr:thesis,
author = {Nina Bohr},
title = {Advances in Reasoning Principles for Contextual Equivalence and Termination},
school = {IT University of Copenhagen},
year = {2007},
}
@article{sumii-pierce-jacm,
author = {Eijiro Sumii and Benjamin Pierce},
title = {A Bisimulation for Type Abstraction and Recursion},
journal = {Journal of the ACM},
volume = 54,
number = 5,
year = 2007,
pages = {1--43},
}
@inproceedings{koutavas-wand-2006,
author = {Vasileios Koutavas and Mitchell Wand},
title = {Small Bisimulations for Reasoning About Higher-Order Imperative Programs},
booktitle = {POPL},
year = {2006},
}
@PhDthesis{ahmed:thesis,
title = {Semantics of Types for Mutable State},
author = "Amal Ahmed",
school = "Princeton University",
year = 2004
}
@Article{johann+:impact,
author = {Patricia Johann and Janis Voigtl\"ander},
title = {The Impact of \emph{seq} on Free Theorems-Based Program Transformations},
journal = {Fundamenta Informaticae},
year = {2006},
volume = {69},
number = {1--2},
pages = {63--102},
}
@InProceedings{johann+:lics10,
author = {Patricia Johann and Alex Simpson and Janis Voigtl\"ander},
title = {A Generic Operational Metatheory for Algebraic Effects},
booktitle = {LICS},
year = {2010},
}
@InProceedings{laird:lics97,
author = {James Laird},
title = {Full Abstraction for Functional Languages with Control},
booktitle = {LICS},
year = {1997},
}
@Article{krivine:realize,
author = {Jean-Louis Krivine},
title = {Classical logic, storage operators and second-order lambda-calculus},
journal = {Annals of Pure and Applied Logic},
year = {1994},
volume = {68},
pages = {53--78},
}
@InProceedings{friedman-haynes,
author = {Daniel Friedman and Christopher Haynes},
title = {Constraining control},
booktitle = {POPL},
year = {1985},
}
@InProceedings{dreyer+:popl10,
author = {Derek Dreyer and Georg Neis and Andreas Rossberg and Lars Birkedal},
title = {A Relational Modal Logic for Higher-Order Stateful {ADTs}},
booktitle = {POPL},
year = {2010},
}
@Article{mason-talcott,
author = {Ian Mason and Carolyn Talcott},
title = {Equivalence in functional languages with effects},
journal = {JFP},
year = {1991},
volume = {1},
number = {3},
pages = {287--327},
}
@InProceedings{thielecke:esop00,
author = {Hayo Thielecke},
title = {On Exceptions versus Continuations in the Presence of State},
booktitle = {ESOP},
year = {2000},
}
@Article{johann:shortcut,
author = {Patricia Johann},
title = {Short Cut Fusion is Correct},
journal = {JFP},
year = {2003},
volume = {13},
number = {4},
pages = {797--814},
}
@InProceedings{neis+:icfp09,
author = {Georg Neis and Derek Dreyer and Andreas Rossberg},
title = {Non-Parametric Parametricity},
booktitle = {ICFP},
year = {2009},
}
@Article{neis+:jfp11,
author = {Georg Neis and Derek Dreyer and Andreas Rossberg},
title = {Non-Parametric Parametricity},
journal = {JFP},
year = {2011},
volume = {21},
number = {4\&5},
pages = {497--562},
}
@Article{dreyer+:lmcs11,
author = {Derek Dreyer and Amal Ahmed and Lars Birkedal},
title = {Logical Step-Indexed Logical Relations},
journal = {LMCS},
year = {2011},
volume = {7},
number = {2:16},
pages = {1--37},
month = jun,
}
@InProceedings{lassen:lics05,
author = {Soren Lassen},
title = {Eager Normal Form Bisimulation},
booktitle = {LICS},
year = {2005},
}
@inproceedings{reynolds-1983,
author = "John C. Reynolds",
title = "Types, abstraction and parametric polymorphism",
booktitle = "Information Processing",
year = 1983,
}
@Article{pierce-sangiorgi,
author = {Benjamin C. Pierce and Davide Sangiorgi},
title = {Behavioral Equivalence in the Polymorphic Pi-Calculus},
journal = {Journal of the ACM},
year = {2000},
volume = {47},
number = {3},
pages = {531--586},
}
@InProceedings{gotsman+:aplas07,
author = {Alexey Gotsman and Josh Berdine and Byron Cook and Noam Rinetzky and Mooly Sagiv},
title = {Local Reasoning About Storable Locks and Threads},
booktitle = {APLAS},
year = {2007},
}
@InProceedings{buisse+:mfps11,
author = {Alexandre Buisse and Lars Birkedal and Kristian St\o{}vring},
title = {A Step-Indexed {Kripke} Model of Separation Logic for Storable Locks},
booktitle = {MFPS},
year = {2011},
}
@Article{sangiorgi:lazy-lambda,
author = {Davide Sangiorgi},
title = {The Lazy Lambda Calculus in a Concurrency Scenario},
journal = {Information and Computation},
year = {1994},
volume = {111},
number = {1},
pages = {120--153},
}
@inproceedings{wadler:free-theorems,
author = "Philip Wadler",
title = "Theorems for free!",
booktitle = {FPCA},
year = 1989,
}
@InProceedings{birkedal+:lics11,
author = {Lars Birkedal and Rasmus Ejlers M\o{}gelberg and Jan Schwinghammer and Kristian St\o{}vring},
title = {First steps in synthetic guarded domain theory: step-indexing in the topos of trees},
booktitle = {LICS},
year = {2011},
}
@InProceedings{ahmed+:icfp11,
author = {Amal Ahmed and Matthias Blume},
title = {An Equivalence-Preserving {CPS} Translation via Multi-Language Semantics},
booktitle = {ICFP},
year = 2011,
}
@Article{uustalu+:njc99,
author = {Tarmo Uustalu and Varmo Vene},
title = {Mendler-style Inductive Types, Categorically},
journal = {Nordic Journal of Computing},
year = {1999},
volume = {6},
number = {3},
pages = {343--361},
}
@Article{mendler:pal91,
author = {Nax P. Mendler},
title = {Inductive Types and Type Constraints in the Second-Order Lambda-Calculus},
journal = {Annals of Pure and Applied Logic},
year = {1991},
volume = {51},
number = {1--2},
pages = {159--172},
}
@InProceedings{koutavas+:mfps11,
author = {Vasileios Koutavas and Paul Blain Levy and Eijiro Sumii},
title = {From Applicative to Environmental Bisimulation},
booktitle = {MFPS},
year = 2011,
}
@InCollection{abramsky:applicative,
author = {Samson Abramsky},
title = {The Lazy Lambda Calculus},
booktitle = {Research Topics in Functional Programming},
pages = {65--117},
editor = {D. A. Turner},
year = 1990,
}
@InProceedings{vafeiadis:mfps11,
author = {Viktor Vafeiadis},
title = {Concurrent separation logic and operational semantics},
booktitle = {MFPS},
year = 2011,
}
@InProceedings{hur+:popl12,
author = {Chung-Kil Hur and Derek Dreyer and Georg Neis and Viktor Vafeiadis},
title = {The Marriage of Bisimulations and {Kripke} Logical Relations},
booktitle = {POPL},
year = {2012},
}
@InProceedings{le+:pldi14,
author = {Vu Le and Mehrdad Afshari and Zhengdong Su},
title = {Compiler Validation via Equivalence Modulo Inputs},
booktitle = {PLDI},
year = {2014},
}
@Article{leroy:compcert,
author = {Xavier Leroy},
title = {A formally verified compiler back-end},
journal = {Journal of Automated Reasoning},
year = {2009},
volume = {43},
number = {4},
pages = {363--446},
}
@InProceedings{perconti+:esop14,
author = {James T. Perconti and Amal Ahmed},
title = {Verifying an Open Compiler Using Multi-Language Semantics},
booktitle = {ESOP},
year = {2014},
}
@InProceedings{matthews+:popl07,
author = {Jacob Matthews and Robert Bruce Findler},
title = {Operational Semantics for Multi-Language Programs},
booktitle = {POPL},
year = {2007},
}
@InProceedings{beringer+:esop14,
author = {Lennart Beringer and Gordon Stewart and Robert Dockins and Andrew W. Appel},
title = {Verified Compilation for Shared-Memory {C}},
booktitle = {ESOP},
year = {2014},
}
@inproceedings{caresl,
title={Unifying refinement and {Hoare}-style reasoning in a logic for higher-order concurrency},
author={Aaron Turon and Derek Dreyer and Lars Birkedal},
booktitle={ICFP},
year={2013},
pages = {377--390},
}
@InProceedings{fcsl,
author = {Aleksandar Nanevski and Ruy Ley-Wild and Ilya Sergey and Germ\'an Andr\'es Delbianco},
title = {Communicating State Transition Systems for Fine-Grained Concurrent Resources},
booktitle = {ESOP},
year = {2014},
pages = {290--310},
}
@InProceedings{tada,
author = {Pedro {da Rocha Pinto} and Thomas Dinsdale-Young and Philippa Gardner},
title = {{TaDA}: A Logic for Time and Data Abstraction},
booktitle = {ECOOP},
year = {2014},
pages = {207--231},
}
@InProceedings{icap,
author = {Kasper Svendsen and Lars Birkedal},
title = {Impredicative Concurrent Abstract Predicates},
booktitle = {ESOP},
year = {2014},
pages = {149--168},
}
@InProceedings{krishnaswami+:icfp12,
author = {Neelakantan R. Krishnaswami and Aaron Turon and Derek Dreyer and Deepak Garg},
title = {Superficially substructural types},
booktitle = {ICFP},
year = {2012},
}
@inproceedings{cap,
title={Concurrent abstract predicates},
author={Dinsdale-Young, T. and Dodds, M. and Gardner, P. and Parkinson, M.
and Vafeiadis, V.},
booktitle={ECOOP},
year={2010},
pages = {504--528},
}
@inproceedings{scsl,
author = {Ley-Wild, Ruy and Nanevski, Aleksandar},
booktitle = {POPL},
title = {Subjective Auxiliary State for Coarse-Grained Concurrency},
year = {2013}
}
@InProceedings{views,
author = {Thomas Dinsdale-Young and Lars Birkedal and Philippa Gardner and Matthew J. Parkinson and Hongseok Yang},
title = {Views: Compositional reasoning for concurrent programs},
booktitle = {POPL},
year = {2013},
}
@article{rg,
author = {Jones, C. B.},
title = {Tentative steps toward a development method for interfering programs},
journal = {TOPLAS},
volume = {5},
number = {4},
year = {1983},
pages = {596--619},
publisher = {ACM},
}
@inproceedings{lrg,
author = {Feng, Xinyu},
title = {Local rely-guarantee reasoning},
booktitle = {POPL},
year = {2009},
pages = {315--327},
}
@inproceedings{rgsep,
title={A marriage of rely/guarantee and separation logic},
author={Vafeiadis, V. and Parkinson, M.},
booktitle={CONCUR},
year={2007},
pages = {256--271},
}
@InProceedings{Parkinson+:popl07,
author={Matthew J. Parkinson and Richard Bornat and Peter W. O'Hearn},
title={Modular verification of a non-blocking stack},
booktitle={POPL},
year={2007},
}
@article{ohearn:csl,
title={Resources, concurrency, and local reasoning},
author={O'Hearn, P.W.},
journal={TCS},
volume={375},
number={1},
pages={271--307},
year={2007},
}
@InProceedings{Elmas+:tacas10,
author={Tayfun Elmas and Shaz Qadeer and Ali Sezgin and Omer Subasi and Serdar Tasiran},
title={Simplifying Linearizability Proofs with Reduction and Abstraction},
booktitle={TACAS},
year={2010},
}
@InProceedings{Elmas+:popl09,
author={Tayfun Elmas and Shaz Qadeer and Serdar Tasiran},
title={A calculus of atomic actions},
booktitle={POPL},
year={2009},
}
@article{linearizability,
author = {Herlihy, Maurice P. and Wing, Jeannette M.},
title = {Linearizability: a correctness condition for concurrent objects},
journal = {TOPLAS},
volume = {12},
number = {3},
year = {1990},
pages = {463--492},
publisher = {ACM},
}
@inproceedings{blaming,
title = {Blaming the client: On data refinement in the presence of pointers},
author = {Filipovi\'{c}, Ivana and O’Hearn, Peter and Torp-Smith, Noah and Yang, Hongseok},
year = 2009,
booktitle = {FACS},
}
@InProceedings{jacobs-piessens,
author = {Bart Jacobs and Frank Piessens},
title = {Expressive modular fine-grained concurrency specification},
booktitle = {POPL},
year = 2011,
}
@Misc{Jacobs:personalcommunication2014,
author = {Bart Jacobs},
title = {Personal communication},
year = {2014},
}
@InProceedings{turon+:popl13,
author = {Aaron Turon and Jacob Thamsborg and Amal Ahmed and Lars Birkedal and Derek Dreyer},
title = {Logical relations for fine-grained concurrency},
booktitle = {POPL},
year = {2013},
}
@InProceedings{elimination-stack,
author = {D. Hendler and N. Shavit and L. Yerushalmi},
title = {A Scalable Lock-Free Stack Algorithm},
booktitle = {SPAA},
year = 2004
}
@Article{lamport:sc,
author={Leslie Lamport},
title={How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs},
journal={IEEE Trans.\ Comput.},
year={1979},
volume={28},
number={9},
pages={690--691},
}
@InProceedings{sagl,
author = {Xinyu Feng and Rodrigo Ferreira and Zhong Shao},
title = {On the relationship between concurrent separation logic and assume-guarantee reasoning},
booktitle = {ESOP},
year = {2007},
pages = {173--188},
}
@Article{owicki-gries:ghost-state,
author = {Susan Owicki and David Gries},
title = {Verifying Properties of Parallel Programs: An Axiomatic Approach},
journal = {CACM},
year = {1976},
volume = {19},
number = {5},
pages = {279--285},
}
@InProceedings{cohen+:imr,
author = {Cohen, Ernie and Alkassar, Eyad and Boyarinov, Vladimir and Dahlweid, Markus and Degenbaev, Ulan and Hillebrand, Mark and Langenstein, Bruno and Leinenbach, Dirk and Moskal, Micha\l and Obua, Steven and Paul, Wolfgang and Pentchev, Hristo and Petrova, Elena and Santen, Thomas and Schirmer, Norbert and Schmaltz, Sabine and Schulte, Wolfram and Shadrin, Andrey and Tobies, Stephan and Tsyban, Alexandra and Tverdyshev, Sergey},
title = {Invariants, Modularity, and Rights},
booktitle = {PSI},
year = {2009},
pages = {43--55},
volume = {5947},
series = {LNCS},
}
@Article{ashcroft:invariants,
author = {Edward A. Ashcroft},
title = {Proving assertions about parallel programs},
journal = {J. Comput. Syst. Sci.},
year = {1975},
volume = {10},
number = {1},
pages = {110--135},
}
@PhdThesis{vafeiadis-thesis,
author = {Viktor Vafeiadis},
title = {Modular fine-grained concurrency verification},
school = {University of Cambridge},
year = {2007},
}
@article{abadi+:speculation,
author = {Mart{\'{\i}}n Abadi and
Leslie Lamport},
title = {The Existence of Refinement Mappings},
journal = {TCS},
year = {1991},
volume = {82},
number = {2},
pages = {253--284},
url = {http://dx.doi.org/10.1016/0304-3975(91)90224-P},
doi = {10.1016/0304-3975(91)90224-P},
timestamp = {Wed, 29 Oct 2014 20:04:49 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/AbadiL91},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{hocap,
author = {Kasper Svendsen and
Lars Birkedal and
Matthew J. Parkinson},
title = {Modular Reasoning about Separation of Concurrent Data Structures},
booktitle = {{ESOP}},
pages = {169--188},
year = {2013},
timestamp = {Mon, 18 Feb 2013 15:03:29 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/SvendsenBP13},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@report{catlogic,
author = {Lars Birkedal and Ale\v{s} Bizjak},
title = {A Taste of Categorical Logic --- Tutorial Notes},
month = oct,
year = {2014},
note = {Available at \url{http://users-cs.au.dk/birke/modures/tutorial/categorical-logic-tutorial-notes.pdf}}
}
@article{dodds:higher-order-sync,
author = {Mike Dodds and
Suresh Jagannathan and
Matthew J. Parkinson and
Kasper Svendsen and
Lars Birkedal},
title = {Verifying Custom Synchronization Constructs Using Higher-Order Separation
Logic},
journal = {TOPLAS},
volume = {38},
number = {2},
pages = {4},
year = {2016},
url = {http://doi.acm.org/10.1145/2818638},
doi = {10.1145/2818638},
timestamp = {Fri, 29 Jan 2016 12:43:32 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/DoddsJPSB16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{iris,
author = {Ralf Jung and
David Swasey and
Filip Sieczkowski and
Kasper Svendsen and
Aaron Turon and
Lars Birkedal and
Derek Dreyer},
title = {Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent
Reasoning},
booktitle = {POPL},
pages = {637--650},
year = {2015},
}
@phdthesis{krebbers:phd,
author = {Robbert Krebbers},
title = {The C standard formalized in Coq},
year = {2015},
school = {Radboud University},
}
@inproceedings{garillot:gonthier:mahboubi:rideau:09,
author = {Fran{\c{c}}ois Garillot and
Georges Gonthier and
Assia Mahboubi and
Laurence Rideau},
title = {Packaging Mathematical Structures},
booktitle = {TPHOLs},
pages = {327--342},
series = {LNCS},
volume = {5674},
year = {2009},
}
@article{spitters:weegen:11,
author = {Bas Spitters and Eelis van der Weegen},
title = {Type classes for mathematics in type theory},
journal = {MSCS},
volume = {21},
number = {4},
pages = {795--825},
year = {2011},
}
@article{sozeau:09,
author = {Matthieu Sozeau},
title = {A New Look at Generalized Rewriting in Type Theory},
journal = {JFR},
volume = {2},
number = {1},
pages = {41--62},
year = {2009},
}
@InProceedings{malecha:esop2016,
author = {Gregory Malecha and Jesper Bengtson},
title = {Easy and efficient automation through reflective tactics},
booktitle = {ESOP},
year = 2016,
}
@inproceedings{gps,
author = {Aaron Turon and
Viktor Vafeiadis and
Derek Dreyer},
title = {{GPS:} navigating weak memory with ghosts, protocols, and separation},
booktitle = {OOPSLA},
pages = {691--707},
year = {2014},
url = {http://doi.acm.org/10.1145/2660193.2660243},
doi = {10.1145/2660193.2660243},
timestamp = {Thu, 16 Oct 2014 09:16:18 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/oopsla/TuronVD14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{birkedal:metric-space,
author = {Lars Birkedal and
Kristian St{\o}vring and
Jacob Thamsborg},
title = {The category-theoretic solution of recursive metric-space equations},
journal = {TCS},
volume = {411},
number = {47},
pages = {4102--4122},
year = {2010},
url = {http://dx.doi.org/10.1016/j.tcs.2010.07.010},
doi = {10.1016/j.tcs.2010.07.010},
timestamp = {Tue, 07 Dec 2010 16:23:22 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/BirkedalST10},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{gotsman:storable-locks,
author = {Alexey Gotsman and
Josh Berdine and
Byron Cook and
Noam Rinetzky and
Mooly Sagiv},
title = {Local Reasoning for Storable Locks and Threads},
booktitle = {APLAS},
pages = {19--37},
year = {2007},
url = {http://dx.doi.org/10.1007/978-3-540-76637-7_3},
doi = {10.1007/978-3-540-76637-7_3},
timestamp = {Thu, 29 Nov 2007 12:28:33 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/aplas/GotsmanBCRS07},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{birkedal:storable-locks,
author = {Alexandre Buisse and
Lars Birkedal and
Kristian St{\o}vring},
title = {Step-Indexed {Kripke} Model of Separation Logic for Storable Locks},
journal = {ENTCS},
volume = {276},
pages = {121--143},
year = {2011},
url = {http://dx.doi.org/10.1016/j.entcs.2011.09.018},
doi = {10.1016/j.entcs.2011.09.018},
timestamp = {Mon, 14 Nov 2011 15:35:16 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/BuisseBS11},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{unification_hints,
author = {Andrea Asperti and
Wilmer Ricciotti and
Claudio Sacerdoti Coen and
Enrico Tassi},
title = {Hints in Unification},
booktitle = {TPHOLs},
pages = {84--98},
year = {2009},
series = {LNCS},
volume = {5674},
}
@inproceedings{bedrock,
author = {Adam Chlipala},
title = {The {Bedrock} structured programming system: combining generative metaprogramming
and {Hoare} logic in an extensible program verifier},
booktitle = {ICFP},
pages = {391--402},
year = {2013},
}
@inproceedings{modures,
author = {Filip Sieczkowski and Ales Bizjak and Lars Birkedal},
title = {{ModuRes}: {A} {Coq} Library for Modular Reasoning About Concurrent Higher-Order
Imperative Programming Languages},
booktitle = {ITP},
pages = {375--390},
year = {2015},
series = {LNCS},
volume = {9236},
}
@inproceedings{fcsl-coq,
author = {Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee},
title = {Mechanized verification of fine-grained concurrent programs},
booktitle = {PLDI},
pages = {77--87},
year = {2015},
url = {http://doi.acm.org/10.1145/2737924.2737964},
doi = {10.1145/2737924.2737964},
timestamp = {Fri, 05 Jun 2015 07:31:54 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/SergeyNB15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{app:14,
editor = {Andrew W. Appel},
title = "{Program Logics for Certified Compilers}",
year = {2014},
publisher = {Cambridge University Press}
}
@inproceedings{charge,
author = {Jesper Bengtson and Jonas Braband Jensen and Lars Birkedal},
title = "{Charge! - {A} Framework for Higher-Order Separation Logic in {C}oq}",
booktitle = {ITP},
year = {2012},
pages = {315--331},
series = {LNCS},
volume = {7406},
}
@inproceedings{jensen:benton:kennedy:13,
author = {Jonas Braband Jensen and
Nick Benton and
Andrew Kennedy},
title = {High-level separation logic for low-level code},
booktitle = {POPL},
pages = {301--314},
year = {2013},
}
@inproceedings{tuch:klein:norrish:07,
author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
title = {Types, bytes, and separation logic},
booktitle = {POPL},
year = {2007},
pages = {97--108},
}