main.bib

@Book{davey-priestley-2002,
  author =       {B.A. Davey and H. Priestly},
  title =        {Introduction to Lattices and Order},
  publisher =    {Cambridge Univ. Press},
  year =         {2002},
  OPTkey =       {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  edition =      {2nd},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}

@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",
}

@Article{reynolds:types,
  author =   {John C. Reynolds},
  title =    {Types, Abstraction, and Parametric Polymorphism},
  journal =      {Information Processing},
  year =     1983,
}

@Article{timany:logrel-in-iris,
  author = 	 {A. Timany and L. Birkedal},
  title = 	 {Type Soundness and Contextual Refinement via
  Logical Relations in Higher-Order Concurrent Separation Logic},
  journal = 	 {},
  year = 	 {2018},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note =	 {Manuscript},
  annote = 	 {Available at \textt{iris-project.org}}
}

@article{DINSDALEYOUNG20181,
title = "A perspective on specifying and verifying concurrent modules",
journal = "Journal of Logical and Algebraic Methods in Programming",
volume = "98",
pages = "1 - 25",
year = "2018",
issn = "2352-2208",
doi = "https://doi.org/10.1016/j.jlamp.2018.03.003",
url = "http://www.sciencedirect.com/science/article/pii/S2352220817300871",
author = "Thomas Dinsdale-Young and Pedro da Rocha Pinto and Philippa Gardner",
keywords = "Concurrency, Specification, Program verification"
}

@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},
  series    = {LNCS},
  volume    = {8586},
}

@InProceedings{hocap-conf,
  author = 	 {K. Svendsen and L. Birkedal and M. Parkinson},
  title = 	 {Modular Reasoning about Separation of Concurrent Data Structures},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of ESOP},
  OPTpages = 	 {},
  year =	 {2013},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =	 {},
  OPTannote = 	 {},
  pdf = {hocap-conf.pdf}
}

@inproceedings{Jacobs:Piessens:2011,
  author    = {Bart Jacobs and Frank Piessens},
  title     = {Expressive modular fine-grained concurrency specification},
  booktitle = {POPL},
  pages     = {271--282},
  year      = {2011},
}


@InProceedings{Hyland:82,
  author = 	 {J.M.E. Hyland},
  title = 	 {The Effective Topos},
  booktitle = 	 {The L.E.J. Brouwer Centenary Symposium},
  editor =	 {A.S. Troelstra and D. van Dalen},
  volume =	 {110},
  series = 	 {Studies in Logic and The Foundations of Mathematics},
  year =	 {1982},
  publisher =	 {North-Holland},
  address =	 {Amsterdam},
  pages =	 {165--216},
  OPTnote = 	 {},
  OPTannote = 	 {}
}


@inproceedings{icap,
  title={Impredicative concurrent abstract predicates},
  author={Svendsen, Kasper and Birkedal, Lars},
  booktitle={European Symposium on Programming Languages and Systems},
  pages={149--168},
  year={2014},
  organization={Springer}
}


@Article{iris-ground-up,
  author =    {Ralf Jung and
               Robbert Krebbers and
               Jacques{-}Henri Jourdan and
               Ale\v{s} Bizjak and
               Lars Birkedal,
               Derek Dreyer},
  title = 	 {Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic},
  journal =  {Journal of Functional Programming},
  year = 	 {2018},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  OPTannote = 	 {}
}

@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},
}


@inproceedings{iris2,
  author    = {Ralf Jung and Robbert Krebbers and Lars Birkedal and
               Derek Dreyer},
  title     = {Higher-order ghost state},
  booktitle = {ICFP},
  pages     = {256--269},
  year      = {2016},
}
                  
@inproceedings{iris3,
  author    = {Robbert Krebbers and
               Ralf Jung and
               Ale\v{s} Bizjak and
               Jacques{-}Henri Jourdan and
               Derek Dreyer and
               Lars Birkedal},
  title     = {The Essence of Higher-Order Concurrent Separation Logic},
  booktitle = {ESOP},
  pages     = {696--723},
  year      = {2017},
  series    = {LNCS}
}

@inproceedings{logrel-fcd,
  author    = {Aaron Joseph Turon and
               Jacob Thamsborg and
               Amal Ahmed and
               Lars Birkedal and
               Derek Dreyer},
  title     = {Logical relations for fine-grained concurrency},
  booktitle = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
               Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25,
               2013},
  pages     = {343--356},
  year      = {2013}
}

@MastersThesis{esben-clausen:msc:hash-tables-in-iris,
  author = 	 {Esben Glavind Clausen},
  title = 	 {Verifying Hash Tables in Iris},
  school = 	 {Aarhus University},
  year = 	 {2017},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {Available at \url{iris-project.org}},
  OPTannote = 	 {}
}

@inproceedings{Krebbers:IPM,
 author = {Krebbers, Robbert and Timany, Amin and Birkedal, Lars},
 title = {Interactive Proofs in Higher-order Concurrent Separation Logic},
 booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
 series = {POPL 2017},
 year = {2017},
 isbn = {978-1-4503-4660-3},
 location = {Paris, France},
 pages = {205--217},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/3009837.3009855},
 doi = {10.1145/3009837.3009855},
 acmid = {3009855},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Coq, Fine-grained Concurrency, Interactive Theorem Proving, Logical Relations, Separation Logic},
}
@book{pierce:tapl,
 author = {Pierce, Benjamin C.},
 title = {Types and Programming Languages},
 year = {2002},
 isbn = {0262162091, 9780262162098},
 edition = {1st},
 publisher = {The MIT Press},
} 
@book{harper:practical-foundations,
 place={Cambridge},
 edition={2},
 title={Practical Foundations for Programming Languages},
 DOI={10.1017/CBO9781316576892},
 publisher={Cambridge University Press},
 author={Harper, Robert},
 year={2016}}