Quelle  root.bib

@STRING{cj="The Computer Journal"}
@STRING{entcs="Electronic Notes on Theoretical Computer Science"}
@STRING{fmsd="Formal Methods in System Design"}
@STRING{fi="Fundamenta Informaticae"}
@STRING{iac="Information and Computation"}
@STRING{jcs="Journal of Computer Security"}
@STRING{jfp="Journal of Functional Programming"}
@STRING{jlc="Journal of Logic and Computation"}
@STRING{jsa="Journal of Systems Architecture"}
@STRING{jucs="Journal of Universal Computing Science"}
@STRING{hosc="Higher-Order and Symbolic Computation"}
@STRING{lncs="LNCS"}
@STRING{mscs="Mathematical Structures in Computer Science"}
@STRING{sttt="International Journal on Software Tools for Technology Transfer"}
@STRING{todaes="ACM Transactions on Design Automation of Electronic Systems"}
@STRING{tocl="ACM Transactions on Computational Logic"}

% NOTE={(A preliminary version of this work appeared as Cambridge Univ.
% Computer Laboratory Tech. Rept. No.~321, December 1993.)},
@ARTICLE{PittsAM:relpod,
 AUTHOR={A.~M.~Pitts},
 TITLE={Relational Properties of Domains},
 JOURNAL={Information and Computation},
 VOLUME=127,
 YEAR=1996,
 PAGES={66--90},
 ABSTRACT={New tools are presented for reasoning about properties of
 recursively defined domains. We work within a general,
 category-theoretic framework for various notions of `relation' on
 domains and for actions of domain constructors on relations.
 Freyd's analysis of recursive types in terms of a property of mixed
 initiality/finality is transferred to a corresponding property of
 {\em invariant\/} relations. The existence of invariant relations is
 proved under completeness assumptions about the notion of relation.
 We show how this leads to simpler proofs of the computational
 adequacy of denotational semantics for functional programming
 languages with user-declared datatypes.  We show how the
 initiality/finality property of invariant relations can be
 specialized to yield an induction principle for admissible subsets
 of recursively defined domains, generalizing the principle of
 structural induction for inductively defined sets. We also show how
 the initiality/finality property gives rise to the co-induction
 principle studied by the author ({\em Theoretical Computer
 Science\/} {\bf 124}, 195--219 (1994)), by which equalities
 between elements of recursively defined domains may be proved via an
 appropriate notion of `bisimulation'.}
}

@inproceedings{DBLP:conf/icalp/Reynolds74,
  author    = {J. C. Reynolds},
  title     = {On the Relation between Direct and Continuation Semantics},
  year      = {1974},
  pages     = {141-156},
  ee        = {https://doi.org/10.1007/3-540-06841-4_57},
  crossref  = {DBLP:conf/icalp/1974},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {3-540-06841-4},
@proceedings{DBLP:conf/icalp/1974,
  editor    = {J. Loeckx},
  title     = {Automata, Languages and Programming, 2nd Colloquium, University
               of Saarbr{\"u}cken, July 29 - August 2, 1974, Proceedings},
  booktitle = {Proceedings of the 2nd Colloquium on Automata, Languages and Programming (ICALP '74)},
  publisher = {Springer},
  series    = LNCS,
  volume    = {14},
  year      = {1974},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{wadler92:_essence_of_funct_progr,
  author =       {P. Wadler},
  title =        {The essence of functional programming (Invited talk)},
  booktitle = "Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '92)",
  year =         {1992},
  address =      {Albuquerque, New Mexico},
  month =        {January}
}

@ARTICLE{Plotkin77,
  AUTHOR = "G. D. Plotkin",
  TITLE = {{LCF} Considered as a Programming Language},
  JOURNAL = TCS,
  YEAR = 1977,
  VOLUME = 5,
  PAGES = {223--255}
}

@InCollection{Sieber:1992,
  author =       "K. Sieber",
  title =        "Reasoning about sequential functions via logical relations",
  booktitle =    "Applications of Categories in Computer Science",
  publisher = "Cambridge University Press",
  year =      1992,
  editor =    "Fourman, M. P. and Johnstone, P. T. and Pitts, A. M.",
  number =    177,
  series =    "LMS Lecture Note Series"
}

@inproceedings{DBLP:conf/mfps/Stoughton93,
  author    = {A. Stoughton},
  title     = {Mechanizing Logical Relations},
  year      = {1993},
  pages     = {359-377},
  ee        = {https://doi.org/10.1007/3-540-58027-1_18},
  crossref  = {DBLP:conf/mfps/1993},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/mfps/Pitts93,
  author    = {A. M. Pitts},
  title     = {Computational Adequacy via ``Mixed'' Inductive Definitions},
  year      = {1993},
  pages     = {72-82},
  ee        = {https://doi.org/10.1007/3-540-58027-1_3},
  crossref  = {DBLP:conf/mfps/1993},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {3-540-58027-1},
@proceedings{DBLP:conf/mfps/1993,
  editor    = {S. D. Brookes and
               M. G. Main and
               A. Melton and
               M. W. Mislove and
               D. A. Schmidt},
  title     = {Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics (MFPS '94)},
  booktitle = {Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics (MFPS '94)},
  publisher = {Springer},
  series    = LNCS,
  volume    = {802},
  year      = {1994},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/ppdp/BentonKBH09,
  author    = {N. Benton and
               A. Kennedy and
               L. Beringer and
               M. Hofmann},
  title     = {Relational semantics for effect-based program transformations:
               higher-order store},
  booktitle = {PPDP},
  year      = {2009},
  pages     = {301-312},
  ee        = {http://doi.acm.org/10.1145/1599410.1599447},
  crossref  = {DBLP:conf/ppdp/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {978-1-60558-568-0},
@proceedings{DBLP:conf/ppdp/2009,
  editor    = {A. Porto and
               F. J. L{\'o}pez-Fraguas},
  title     = {Proceedings of the 11th International ACM SIGPLAN Conference
               on Principles and Practice of Declarative Programming, September
               7-9, 2009, Coimbra, Portugal},
  booktitle = {PPDP},
  publisher = {ACM},
  year      = {2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Winskel:1993,
 author = {Winskel, G.},
 title = {The Formal Semantics of Programming Languages},
 year = {1993},
 publisher = {MIT Press},
 address = "Cambridge, MA"
}

@Book{Mitchell:1996,
  author       = {J. C. Mitchell},
  title        = {Foundations for Programming Languages},
  publisher    = {MIT Press},
  address = "Cambridge, MA",
  year         = 1996,
  series       = {Foundations of Computing},
}

@article{DBLP:journals/tcs/Filinski07,
  author    = {A. Filinski},
  title     = {On the relations between monadic semantics},
  journal   = TCS,
  volume    = {375},
  number    = {1-3},
  year      = {2007},
  pages     = {41-75},
  ee        = {https://doi.org/10.1016/j.tcs.2006.12.027},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{Plotkin:1973,
  author =       {G. D. Plotkin},
  title =        {Lambda-definability and logical relations},
  institution =  {School of Artificial Intelligence, Unversity of Edinburgh},
  year =         1973,
  number =    {SAI-RM-4}
}

@article{DBLP:journals/jar/Nipkow01,
  author    = {T. Nipkow},
  title     = "More {Church-Rosser} Proofs",
  journal   = {Journal of Automated Reasoning},
  volume    = {26},
  number    = {1},
  year      = {2001},
  pages     = {51-66},
  ee        = {https://doi.org/10.1023/A:1006496715975},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/fac/Nipkow98,
  author    = {T. Nipkow},
  title     = {Winskel is (almost) Right: Towards a Mechanized Semantics},
  journal   = {Formal Aspects of Computing},
  volume    = {10},
  number    = {2},
  year      = {1998},
  pages     = {171-186},
  ee        = {https://doi.org/10.1007/s001650050009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/tphol/NorrishV07,
  author    = {M. Norrish and
               R. Vestergaard},
  title     = {Proof Pearl: {de Bruijn} Terms Really Do Work},
  year      = {2007},
  pages     = {207-222},
  ee        = {https://doi.org/10.1007/978-3-540-74591-4_16},
  crossref  = {DBLP:conf/tphol/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {978-3-540-74590-7},
@proceedings{DBLP:conf/tphol/2007,
  editor    = {K. Schneider and
               J. Brandt},
  title     = {Theorem Proving in Higher Order Logics, 20th International
               Conference, TPHOLs 2007, Kaiserslautern, Germany, September
               10-13, 2007, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = LNCS,
  volume    = {4732},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/jacm/SethiT80,
  author    = {R. Sethi and A. Tang},
  title     = {Constructing Call-by-Value Continuation Semantics},
  journal   = JACM,
  volume    = {27},
  number    = {3},
  year      = {1980},
  pages     = {580-597},
  ee        = {http://doi.acm.org/10.1145/322203.322216},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/KoutavasW06,
  author    = {V. Koutavas and M. Wand},
  title     = {Small bisimulations for reasoning about higher-order imperative
               programs},
  year      = {2006},
  pages     = {141-152},
  ee        = {http://doi.acm.org/10.1145/1111037.1111050},
  crossref  = {DBLP:conf/popl/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/DanielssonHJG06,
  author    = {N. A. Danielsson and
               J. Hughes and
               P. Jansson and
               J. Gibbons},
  title     = {Fast and loose reasoning is morally correct},
  year      = {2006},
  pages     = {206-217},
  ee        = {http://doi.acm.org/10.1145/1111037.1111056},
  crossref  = {DBLP:conf/popl/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  title     = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on
%               Principles of Programming Languages, POPL 2006, Charleston,
%               South Carolina, USA, January 11-13, 2006},
%  isbn      = {1-59593-027-2},
@proceedings{DBLP:conf/popl/2006,
  editor    = {J. G. Morrisett and
               S. L. Peyton Jones},
  title = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages (POPL '06)},
  booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages (POPL '06)},
  publisher = {ACM},
  year      = {2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/icfp/WandV04,
  author    = {M. Wand and D. Vaillancourt},
  title     = {Relating models of backtracking},
  year      = {2004},
  pages     = {54-65},
  ee        = {http://doi.acm.org/10.1145/1016850.1016861},
  crossref  = {DBLP:conf/icfp/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {1-58113-905-5},
@proceedings{DBLP:conf/icfp/2004,
  editor    = {C. Okasaki and K. Fisher},
  title     = {Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP '04)},
  booktitle = {Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP '04)},
  publisher = {ACM},
  year      = {2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Huffman:MonadTransformers:2012,
  author = "B. Huffman",
  title     = {Formal Verification of Monad Transformers},
  booktitle = {ICFP 2012},
  year      = 2012,
}

@inproceedings{DBLP:conf/tphol/BentonKV09,
  author    = {N. Benton and
               A. Kennedy and
               C. Varming},
  title     = {Some Domain Theory and Denotational Semantics in Coq},
  booktitle = {TPHOLs},
  year      = {2009},
  pages     = {115-130},
  ee        = {https://doi.org/10.1007/978-3-642-03359-9_10},
  crossref  = {DBLP:conf/tphol/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {978-3-642-03358-2},
@proceedings{DBLP:conf/tphol/2009,
  editor    = {S. Berghofer and
               T. Nipkow and
               C. Urban and
               M. Wenzel},
  title     = {Theorem Proving in Higher Order Logics, 22nd International
               Conference, TPHOLs 2009, Munich, Germany, August 17-20,
               2009. Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = LNCS,
  volume    = {5674},
  year      = {2009},
  ee        = {https://doi.org/10.1007/978-3-642-03359-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@phdthesis{holcf11,
  author = {B. Huffman},
  title = {HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs},
  school = {Portland State University},
  year = {2012}
}

@article{HOLCF:1999,
  author = {M\"uller, O. and Nipkow, T. and von Oheimb, D. and Slotosch, O.},
  title = "{HOLCF = HOL + LCF}",
  journal=jfp,
  volume=9,
  pages={191--223},
  year=1999
}

@inproceedings{DBLP:conf/tlca/Sieber93,
  author    = {K. Sieber},
  title     = {Call-by-Value and Nondeterminism},
  year      = {1993},
  pages     = {376-390},
  ee        = {https://doi.org/10.1007/BFb0037119},
  crossref  = {DBLP:conf/tlca/1993},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/tlca/1993,
  editor    = {M. Bezem and
               J. F. Groote},
  title     = {Typed Lambda Calculi and Applications, International Conference
               on Typed Lambda Calculi and Applications, TLCA '93, Utrecht,
               The Netherlands, March 16-18, 1993, Proceedings},
  booktitle = {Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA '93)},
  publisher = {Springer},
  series    = LNCS,
  volume    = {664},
  year      = {1993},
  isbn      = {3-540-56517-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/programm/Hennessy82,
  author    = {M. Hennessy},
  title     = {Powerdomains and nondeterministic recursive definitions},
  booktitle = {Symposium on Programming},
  year      = {1982},
  pages     = {178-193},
  ee        = {https://doi.org/10.1007/3-540-11494-7_13},
  crossref  = {DBLP:conf/programm/1982},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/programm/1982,
  editor    = {M. Dezani-Ciancaglini and
               U. Montanari},
  title     = {International Symposium on Programming, 5th Colloquium,
               Torino, Italy, April 6-8, 1982, Proceedings},
  booktitle = {Symposium on Programming},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {137},
  year      = {1982},
  isbn      = {3-540-11494-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/ppdp/BentonKBH07,
  author    = {N. Benton and
               A. Kennedy and
               L. Beringer and
               M. Hofmann},
  title     = {Relational semantics for effect-based program transformations
               with dynamic allocation},
  booktitle = {PPDP},
  year      = {2007},
  pages     = {87-96},
  ee        = {http://doi.acm.org/10.1145/1273920.1273932},
  crossref  = {DBLP:conf/ppdp/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {978-1-59593-769-8},
@proceedings{DBLP:conf/ppdp/2007,
  editor    = {M. Leuschel and
               A. Podelski},
  title     = {Proceedings of the 9th International ACM SIGPLAN Conference
               on Principles and Practice of Declarative Programming, July
               14-16, 2007, Wroclaw, Poland},
  booktitle = {PPDP},
  publisher = {ACM},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/siamcomp/MossesP87,
  author    = {P. D. Mosses and
               G. D. Plotkin},
  title     = {On Proving Limiting Completeness},
  journal   = {SIAM J. Comput.},
  volume    = {16},
  number    = {1},
  year      = {1987},
  pages     = {179-194},
  ee        = {https://doi.org/10.1137/0216015},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {978-0-13-562132-5},
%  series    = {Prentice-Hall international series in computer science},
@book{DBLP:books/daglib/0002432,
  author    = {J. W. de Bakker and
               A. de Bruin and
               J. Zucker},
  title     = {Mathematical theory of program correctness},
  publisher = {Prentice-Hall},
  year      = {1980},
  pages     = {I-XV, 1-505},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

% isbn = {0-262-07143-6},
@book{Gunter:1992,
 author = {Gunter,, C. A.},
 title = "{S}emantics of {P}rogramming {L}anguages: {S}tructures and {T}echniques",
 year = {1992},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
}

@article{DBLP:journals/entcs/UrbanN09,
  author    = {C. Urban and
               J. Narboux},
  title     = {Formal SOS-Proofs for the Lambda-Calculus},
  journal   = entcs,
  volume    = {247},
  year      = {2009},
  pages     = {139-155},
  ee        = {https://doi.org/10.1016/j.entcs.2009.07.053},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/hopl/HudakHJW07,
  author    = {P. Hudak and
               J. Hughes and
               S. L. Peyton Jones and
               P. Wadler},
  title     = {A history of Haskell: being lazy with class},
  booktitle = {HOPL},
  year      = {2007},
  pages     = {1-55},
  ee        = {http://doi.acm.org/10.1145/1238844.1238856},
  crossref  = {DBLP:conf/hopl/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/hopl/2007,
  editor    = {B. G. Ryder and
               B. Hailpern},
  title     = {Proceedings of the Third ACM SIGPLAN History of Programming
               Languages Conference (HOPL-III), San Diego, California,
               USA, 9-10 June 2007},
  booktitle = {HOPL},
  publisher = {ACM},
  year      = {2007},
  ee        = {http://dl.acm.org/citation.cfm?id=1238844},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{Mulmuley:1987,
  author =    "K. Mulmuley",
  title =        "Full Abstraction and Semantic Equivalence",
  publisher =    "MIT Press",
  year =         1987}


@book{Stoy:1977,
 author = {J. E. Stoy},
 title = "Denotational Semantics: The {S}cott-{S}trachey Approach to Programming Language Theory",
 year = {1977},
 publisher = {MIT Press},
}

@article{DBLP:journals/siamcomp/Scott76,
  author    = {D. S. Scott},
  title     = "{D}ata {T}ypes as {L}attices",
  journal   = {SIAM J. Comput.},
  volume    = {5},
  number    = {3},
  year      = {1976},
  pages     = {522-587},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}