@inproceedings{Abadi:90,
 title = "A Per Model of Polymorphism and Recursive Types",
 author = "Abadi, Mart{\'i}n and Plotkin, Gordon D.",
 booktitle = "Logic in Computer Science",
 year = 1990,
}

@incollection{Abramsky:94,
  author = 	{Samson Abramsky and Achim Jung},
  booktitle = 	{Handbook of Logic in Computer Science},
  title = 	{Domain Theory},
  year = 	1994,
}

@phdthesis{Ahmed:04,
  author =       {Ahmed, Amal Jamil},
  title =        {Semantics of Types for Mutable State},
  year =         2004,
  school = "Department of Computer Science, Princeton University",
}

@inproceedings{Ahmed:06,
  author =       {Ahmed, Amal},
  title =        {Step-Indexed Syntactic Logical Relations for
                  Recursive and Quantified Types},
  booktitle =       {European Symposium on Programming},
  year =         2006,
}

@inproceedings{Allen:87,
 author = "Allen, Stuart",
 title = "A Non-Type-Theoretic Definition of {Martin-L\"{o}f}'s Types",
 booktitle = "Logic and Computer Science",
 year = 1987,
}


@inproceedings{America:87,
  author =       {America, Pierre and Rutten, Jan J. M. M.},
  title =        {Solving Reflexive Domain Equations in a Category of
                  Complete Metric Spaces},
  booktitle =    {Workshop on Mathematical Foundations of Programming Language Semantics},
  year =         1988,
}

@article{Appel:01,
  author =       {Appel, Andrew W. and McAllester, David},
  title =        {An Indexed Model of Recursive Types for Foundational
                  Proof-carrying Code},
  journal =      {ACM Transactions Programming Language Systems},
  year =         2001,
}

@inproceedings{Appel:07,
  author =       {Appel, Andrew W. and Melli\`{e}s, Paul-Andr{\'e} and
                  Richards, Christopher D. and Vouillon,
                  J{\'e}r\^{o}me},
  title =        {A Very Modal Model of a Modern, Major, General Type
                  System},
  booktitle =    {Principles of Programming Languages},
  year =         2007,
}

@InProceedings{Atkey:12,
  title = {Relational Parametricity for Higher Kinds},
  author = {Robert Atkey},
  year = {2012},
  booktitle = {Computer Science Logic},
}

@inproceedings{Bahr:17,
  title =        {{The Clocks Are Ticking: No More Delays!}},
  author =       {Bahr, Patrick and Grathwohl, Hans Bugge and
                  M{\o}gelberg, Rasmus Ejlers},
  year =         2017,
  booktitle =    {Logic in Computer Science},
}

@article{Bainbridge:90,
  title =        "Functorial polymorphism",
  journal =      "Theoretical Computer Science",
  year =         1990,
  author =       "E.S. Bainbridge and P.J. Freyd and A. Scedrov and
                  P.J. Scott"
}

@book{Barendregt:13,
  title={The Lambda Calculus: Its Syntax and Semantics},
  author={Barendregt, Henk},
  series={Studies in Logic and the Foundations of Mathematics},
  year={2013},
  publisher={Elsevier Science}
}

@inproceedings{Birkedal:05,
  author = {Lars Birkedal and Rasmus M{\o}gelberg},
  title = {{Categorical models for Abadi and Plotkin’s logic for parametricity}},
  year = 2005,
  booktitle = {Mathematical Structures in Computer Science}
}


@InProceedings{Birkedal:13,
  author = 	 {Lars Birkedal and Rasmus M{\o}gelberg},
  title = 	 {Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes},
  booktitle = {Logic in Computer Science},
  year = 	 2013,
}


@InProceedings{Birkedal:16,
  author =       {Birkedal, Lars and Bizjak, Ale{\v{s}} and Clouston, Ranald and
                  Gratwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea},
  title =        {Guarded Cubical Type Theory},
  booktitle =    {TYPES},
  year =         2016,
}

@Article{Birkedal:99,
  author =       {Birkedal, Lars and Harper, Robert},
  title =        {Constructing Interpretations of Recursives Types in
                  an Operational Setting},
  journal =      {Information and Computation},
  year =         1999,
}

@article{Birkedal:adts:12,
  author = 	 {Lars Birkedal and Kristen St{\o}vring and Jacob Thamsborg},
  title = 	 {A Relational Realizability Model for Higher-Order Stateful {ADT}s},
  journal = 	 {Logic and Algebraic Programming},
  year = 	 2012,
}

@article{Birkedal:domain:10,
 author = {Birkedal, Lars and St{\o}vring, Kristian and Thamsborg, Jacob},
 title = {The Category-theoretic Solution of Recursive Metric-space Equations},
 journal = {Theoretical Computer Science},
 year = {2010},
}

@InProceedings{Birkedal:guarded:10,
  author =       {Lars Birkedal and Jan Schwinghammer and Kristian St{\o}vring},
  title =        {A Metric Model of Lambda Calculus with Guarded Recursion},
  year =         2010,
  booktitle =   {Fixed Points in Computer Science},
}

@article{Birkedal:realizability:10,
  author =       {Birkedal, Lars and St{\o}vring, Kristian and Thamsborg, Jacob},
  title =        {Realizability Semantics of Parametric Polymorphism,
                  General References, and Recursive Types},
  journal =      {Mathematical Structures in Computer Science},
  year =         2010,
}


@InProceedings{Birkedal:recursive:11,
  author =       {Birkedal, Lars and Reus, Bernhard and Schwinghammer, Jan and
                  St{\o}vring, Kristian and Thamsborg, Jacob and Yang, Hongseok},
  title =        {Step-Indexed Kripke Models over Recursive Worlds},
  booktitle =    {Principles of Programming Languages},
  year =         2011,
}

@inproceedings{Birkedal:steps:11,
  title =        {First Steps in Synthetic Guarded Domain Theory:
                  Step-Indexing in the Topos of Trees},
  author =       {Birkedal, Lars and M{\o}gelberg, Rasmus Ejlers and
                  Schwinghammer, Jan and St{\o}vring, Kristian},
  booktitle =    {Logic in Computer Science},
  year =         2011
}

@misc{Birkedal:trans:12,
  author =       {Lars Birkedal},
  title =        {A note on the transitivity of step-indexed logical
                  relations},
  year =         2012
}

@InProceedings{Bizjak:16,
  author =       {Bizjak, Ale{\v{s}} and Grathwohl, Hans Bugge and Clouston, Ranald and
                  M{\o}gelberg, Rasmus Ejlers and Birkedal, Lars},
  title =        {Guarded Dependent Type Theory with Coinductive Types},
  booktitle =    {Foundations of Software Science and Computation Structures},
  year =         2016,
}

@article{Crary:07,
  author =       {Crary, Karl and Harper, Robert},
  title =        {Syntactic Logical Relations for Polymorphic and
                  Recursive Types},
  journal =      {Electronic Notes Theoretical Computer Science},
  year =         2007,
}

@inproceedings{Crary:17,
 author = {Crary, Karl},
 title = {Modules, Abstraction, and Parametric Polymorphism},
 booktitle = {Principles of Programming Languages},
 year = {2017},
}

@INPROCEEDINGS{Crary:99,
  AUTHOR = {Karl Crary and Stephanie Weirich},
  TITLE = {Flexible Type Analysis},
  BOOKTITLE = {International Conference on Functional Programming},
  YEAR = 1999,
}

@article{Davies:01,
 author = "Rowan Davies and Frank Pfenning",
 title = "A Modal Analysis of Staged Computation",
 journal = "Journal of the {ACM}",
 year = 2001,
}

@inproceedings{Dreyer:09,
  author =       {Dreyer, Derek and Ahmed, Amal and Birkedal, Lars},
  title =        {Logical Step-Indexed Logical Relations},
  booktitle =    {Logic In Computer Science},
  year =         2009,
}

@inproceedings{Dreyer:10,
  author =       {Dreyer, Derek and Neis, Georg and Birkedal, Lars},
  title =        {The Impact of Higher-order State and Control Effects
                  on Local Relational Reasoning},
  booktitle =      {International Conference on Functional Programming},
  year =         2010,
}

@inproceedings{Dunphy:04,
  title = {Parametric Limits},
  author = {Brian Dunphy and Uday Reddy},
  year = {2004},
  booktitle = {Logic in Computer Science}
}

@inproceedings{Escardo:98,
  author =       {Mart{\'i}n Escard{\'o}},
  title =        {A metric model of PCF},
  booktitle =    {Workshop on Realizability Semantics and Applications},
  year =         1998
}

@inproceedings{Freyd:70,
  author =       {Freyd, Peter},
  year =         1970,
  booktitle =    {Category Theory},
  title =        {Algebraically complete categories}
}

@inproceedings{Girard:71,
 author = "Jean-Yves Girard",
 title = "Une extension de l'interpr\'{e}tation de {G\"{o}del} \`{a} l'analyse, et son application \`{a} l'\'{e}limination de coupures dans l'analyse et la th\'{e}orie des types",
 booktitle = "Proceedings of the Second Scandinavian Logic Symposium",
 year = 1971,
}

@phdthesis{Girard:72,
 author = "Jean-Yves Girard",
 title = "Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur",
 school = "Universit\'{e} Paris VII",
 year = 1972,
}

@article{Girard:93,
 author = "Jean-Yves Girard",
 title = "On the unity of logic",
 journal = "Annals of Pure and Applied Logic",
 year = 1993,
 volume = 59,
 number = 3,
}

@book{Girez:03,
  title =        {Continuous Lattices and Domains},
  author =       {Gierz, G. and Hofmann, K. H. and Keimel, K. and
                  Lawson, J. D. and Mislove, M. and Scott, D. S. and
                  Rota, G.-C.},
  year =         2003
}

@book{Harper:16,
  title={Practical Foundations for Programming Languages},
  author={Harper, Robert},
  year={2016},
  publisher={Cambridge University Press}
}

@article{Harper:92,
 author = "Harper, Robert",
 title = "Constructing Type Systems over an Operational Semantics",
 journal = "Journal of Symbolic Computation",
 year = 1992,
}

@article{Hasegawa:94,
  author =       {Hasegawa, Ryu},
  year =         1994,
  title =        {Categorical Data Types in Parametric Polymorphism.},
  booktitle =    {Mathematical Structures in Computer Science}
}

@article{Hermida:14,
  author =       {Hermida, Claudio and Reddy, Uday and Robinson,
                  Edmund},
  year =         2014,
  title =        {Logical Relations and Parametricity – A Reynolds
                  Programme for Category Theory and Programming
                  Languages},
  booktitle =    {Electronic Notes in Theoretical Computer Science}
}

@misc{Hofmann:90s,
 author = {Martin Hofmann and Thomas Steicher},
 title = {Lifting Grothendieck Universes},
 year = {199?},
 note = {Unpublished note, available online at
 \url{http://www.mathematik.tu−darmstadt.de/~streicher/NOTES/lift.dvi.gz}}
}

@INPROCEEDINGS{Howe:98,
  author =       {Douglas J. Howe},
  title =        {Equality In Lazy Computation Systems},
  booktitle =       {Logic in Computer Science},
  year =         1989,
}

@inproceedings{Hur:bisim:12,
 author = "Hur, Chung-Kil and Dreyer, Derek and Neis, Georg and Vafeiadis, Viktor",
 title = "The Marriage of Bisimulations and {Kripke} Logical Relations",
 booktitle = "Principles of Programming Languages",
 year = 2012,
}

@techreport{Hur:rts:12,
 title = "The Transitive Composability of Relation Transition Systems",
 author = "Hur, Chung-Kil and Neis, Georg and Dreyer, Derek and Vafeiadis, Viktor",
 year = 2012,
 institution = "Max Planck Institute for Sofware Systems",
 number = "MPI-SWS-2012-002",
}

@article{Jung:15,
  author =       {Jung, Ralf and Swasey, David and Sieczkowski, Filip
                  and Svendsen, Kasper and Turon, Aaron and Birkedal,
                  Lars and Dreyer, Derek},
  title =        {Iris: Monoids and Invariants As an Orthogonal Basis
                  for Concurrent Reasoning},
  journal =      {Principles of Programming Languages},
  year =         2015,
}

@inproceedings{Jung:16,
  author =       {Jung, Ralf and Krebbers, Robbert and Birkedal, Lars
                  and Dreyer, Derek},
  title =        {Higher-order Ghost State},
  booktitle =       {International Conference on Functional Programming},
  year =         2016,
}

@Article{Jung:17,
  author =       {Jung, Ralf and Krebbers, Robert and Jourdan, Jacques-Henri and
                  Bizjak, Ale{\v{s}} and Birkedal, Lars and Dreyer, Derek},
  title =        {Iris from the Ground Up: A Modular Foundation for
                  Higher-Order Concurrent Separation Logic},
  journal =      {Submitted for publication},
  year =         2017,
}

@inproceedings{Krebbers:17,
  author =       "Krebbers, Robbert and Jung, Ralf and Bizjak,
                  Ale{\v{s}} and Jourdan, Jacques-Henri and Dreyer,
                  Derek and Birkedal, Lars",
  title =        "The Essence of Higher-Order Concurrent Separation Logic",
  bookTitle =    "European Joint Conferences on Theory and Practice of Software",
  year =         2017,
}

@article{Krivine:94,
  title =        "Classical logic, storage operators and second-order
                  lambda-calculus",
  journal =      "Annals of Pure and Applied Logic",
  year =         1994,
  author =       "Jean-Louis Krivine",
}

@InProceedings{Krogh-Jespersen:17,
  author =       {M. Krogh-Jespersen and K. Svendsen and L. Birkedal},
  title =        {A Relational Model of Types-and-Effects in
                  Higher-Order Concurrent Separation Logic},
  booktitle =    {Principles of Programming Languages},
  year =         2017,
}

@inproceedings{Ma:91,
  author =       {Ma, QingMing and C. Reynolds, John},
  year =         1991,
  booktitle =      {Mathematical Foundations of Programming Semantics},
  title =        {Types, Abstractions, and Parametric Polymorphism,
                  Part 2.}
}

@article{Mitchell:91,
  title =        "Kripke-style models for typed lambda calculus",
  journal =      "Annals of Pure and Applied Logic",
  year =         1991,
  author =       "John C. Mitchell and Eugenio Moggi"
}

@book{Munkres:00,
  title={Topology},
  author={Munkres, James R.},
  year={2000},
  publisher="Pearson",
}

@inproceedings{Nakano:00,
  author =       {Nakano, Hiroshi},
  title =        {A Modality for Recursion},
  booktitle =    {Logic in Computer Science},
  year =         2000,
}

@inproceedings{Nakano:01,
 author = "Hiroshi Nakano",
 title = "Fixed-point logic with the approximation modality and its Kripke completeness",
 booktitle = "Theoretical Aspects of Computer Software",
 year = 2001,
}

@InProceedings{Paviotti:15,
  author = 	 {M. Paviotti and R.E. M{\o}gelberg and L. Birkedal},
  title = 	 {A Model of {PCF} in Guarded Type Theory},
  booktitle =	 {Mathematical Foundations of Programming Semantics},
  year = 	 2015,
}

@article{Pfenning:01,
  author =       {Pfenning, Frank and Davies, Rowan},
  title =        {A Judgmental Reconstruction of Modal Logic},
  journal =      {Mathematical Structures in Computer Science},
  year =         2001,
}

@InCollection{Pitts:11,
  author =       {Pitts, Andrew M.},
  title =        {Howe's Method for Higher-Order Languages},
  booktitle =    {Advanced Topics in Bisimulation and Coinduction},
  year =         2011,
}

@book{Pitts:13,
  title={Nominal Sets: Names and Symmetry in Computer Science},
  author={Pitts, Andrew M.},
  year={2013},
  publisher={Cambridge University Press}
}

@article{Pitts:96,
  author =       {Pitts, Andrew M.},
  title =        {Relational Properties of Domains},
  journal =      {Information and Computation},
  year =         1996,
}

@incollection{Pitts:97,
 author = "Pitts, Andrew M.",
 title = "Operationally-Based Theories of Program Equivalence",
 booktitle = "Semantics and Logics of Computation",
 year = 1997,
 publisher = "Cambridge University Press",
}

@incollection{Pitts:98,
  author =       {Pitts, Andrew M. and Stark, Ian D. B.},
  title =        {Operational Reasoning for Functions with Local
                  State},
  booktitle =    {Higher Order Operational Techniques in Semantics},
  year =         1998,
}

@article{Plotkin:80,
  title={Lambda-definability in the full type hierarchy},
  author={Plotkin, Gordon},
  journal={To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
  year={1980}
}

@inproceedings{Pottier:11,
  author =       {Pottier, Fran\c{c}ois},
  title =        {A typed store-passing translation for general
                  references},
  booktitle =    {Principles of Programming Languages},
  year =         2011,
}

@inproceedings{Reynolds:83,
  author = {Reynolds, John C.},
  title = {Types, Abstraction, and Parametric Polymorphism},
  booktitle = {Information Processing},
  year = {1983},
}

@inproceedings{Robinson:94,
  author =       {Robinson, Edmund and Rosolini, Giuseppe},
  year =         1994,
  title =        {Reflexive graphs and parametric polymorphism},
  booktitle =    {Logic in Computer Science}
}

@article{Scott:76,
  author =       {Scott, Dana},
  year =         1976,
  title =        {Data Types as Lattices},
  journal =      {SIAM Journal on Computing}
}

@inproceedings{Smyth:77,
  author =       {Smyth, Michael and Plotkin, Gordon},
  year =         1977,
  title =        {The Category-Theoretic Solution of Recursive Domain
                  Equations},
  booktitle =    {SIAM Journal on Computing}
}

@misc{Streicher:04,
  author = {Thomas Streicher},
  title = {Universes in Toposes},
  year = 2004,
  note = {Unpublished note, available online at
  \url{http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/UniTop.pdf}}
}

@inproceedings{Svendsen:16,
  author =       "Svendsen, Kasper and Sieczkowski, Filip and
                  Birkedal, Lars",
  title =        "Transfinite Step-Indexing: Decoupling Concrete and
                  Logical Steps",
  bookTitle =    "European Symposium on Programming",
  year =         2016,
}

@article{Tait:67,
  author =       "Tait, William W.",
  journal =      "Journal of Symbolic Logic",
  title =        {{Intensional Interpretations of Functionals of Finite
                  Type I}},
  year =         1967
}

@inproceedings{Turon:13,
  author =       {Turon, Aaron J. and Thamsborg, Jacob and Ahmed, Amal
                  and Birkedal, Lars and Dreyer, Derek},
  title =        {Logical Relations for Fine-grained Concurrency},
  booktitle =       {Principles of Programming Languages},
  year =         2013,
}

@inproceedings{Vytiniotis:10,
  author =       {Vytiniotis, Dimitrios and Weirich, Stephanie},
  title =        {Parametricity, type equality, and higher-order
                  polymorphism},
  booktitle =    {Journal of Functional Programming},
  year =         2010,
}

@Manual{coq,
  title =        {The Coq proof assistant reference manual},
  author =       {\mbox{The Coq development team}},
  organization = {LogiCal Project},
  year =         2004,
  url =          "http://coq.inria.fr"
}