@book{EdR:cup98,
  author = {W.-P. de Roever and K. Engelhardt},
  title = {Data Refinement: Model-Oriented Proof Methods and
                  their Comparison},
  publisher = {Cambridge University Press},
  pages = 430,
  year = 1998,
  annote = {With the assistance of Jos Coenen, Karl-Heinz Buth,
                  Paul Gardiner, Yassine Lakhnech, and Frank
                  Stomp},
  annote = {$\pounds$45\,/\,US\$69.95\,/\,AU\$125},
  http = {http://www.informatik.uni-kiel.de/~bkmail1/}
}

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

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

@book{Manna:1974,
 author = {Manna, Z.},
 title = {Introduction to Mathematical Theory of Computation},
 year = {1974},
 isbn = {0070399107},
 publisher = {McGraw-Hill, Inc.},
 address = {New York, NY, USA},
}

@Book{Greibach:1975,
  author =       "S. Greibach",
  title =        "{Theory of program structures: schemes, semantics,
                 verification}",
  volume =       36,
  publisher =    "Springer-Verlag",
  pages =        389,
  year =         1975,
  series =       {LNCS},
}

@inproceedings{DBLP:conf/tphol/Huffman09,
  author    = {B. Huffman},
  title     = {A Purely Definitional Universal Domain},
  booktitle = "{TPHOL}s",
  year      = {2009},
  pages     = {260-275},
  ee        = {https://doi.org/10.1007/978-3-642-03359-9_19},
  crossref  = {DBLP:conf/tphol/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@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},
  isbn      = {978-3-642-03358-2},
  ee        = {https://doi.org/10.1007/978-3-642-03359-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Gammie:2011,
  author =       {P. Gammie},
  title =        {Short Note: Strict unwraps make worker/wrapper fusion totally correct},
  journal =      {Journal of Functional Programming},
  year =         2011,
  volume =       21,
  pages =        {209-213}
}

@inproceedings{barbed-wire:1991,
	abstract = {We develop a calculus for lazy functional programming based on recursion operators associated with data type definitions. For these operators we derive various algebraic laws that are useful in deriving and manipulating programs. We shall show that all example functions in Bird and Wadler's "Introduction to Functional Programming" can  expressed using these operators.},
	author = {E. Meijer and M. Fokkinga and R. Paterson},
	booktitle = "{P}roceedings of the {C}onference on {F}unctional {P}rogramming and {C}omputer {A}rchitecture",
	keywords = {anamorphism, bifunctors, catamorphism, fold, functors, hylomorphism, lazy-evaluation, paramorphism, program-calculation, unfold},
	pages = {124--144},
	posted-at = {2008-08-18 18:44:21},
	priority = {2},
	publisher = {Springer-Verlag},
	title = {Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire},
	year = {1991}
}

@TechReport{FokkingaMeijer:1991,
  author =       {M. M. Fokkinga and Erik Meijer},
  title =        "{P}rogram {C}alculation {P}roperties of {C}ontinuous {A}lgebras",
  institution =  {CWI},
  year =         1991,
  number =    "CS-R9104"
}

@article{GillHutton:2009,
  author = {A. Gill and G. Hutton},
  title = {The worker/wrapper transformation},
  abstract = {The worker/wrapper transformation is a technique for changing the type of a computation, usually with the aim of improving its performance. It has been used by compiler writers for many years, but the technique is little-known in the wider functional programming community, and has never been described precisely. In this article we explain, formalise, and explore the generality of the worker/wrapper transformation. We also provide a systematic recipe for its use as an equational reasoning technique for improving the performance of programs, and illustrate the power of this recipe using a range of examples.},
  journal = "{J}ournal of {F}unctional {P}rogramming",
  publisher = {Cambridge University Press},
  volume = {19},
  number = {2},
  pages = {227--251},
  month = {March},
  year = {2009}
}

@Unpublished{Plotkin:1983,
  author =       {G. Plotkin},
  title =        "{P}isa {N}otes (on {D}omain {T}heory)",
  note =         {Unpublished},
  year =      1983,
  url = "http://homepages.inf.ed.ac.uk/gdp/publications/Domains.ps"
}

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

@phdthesis{Tullsen:PhDThesis,
 author = {M. Tullsen},
 title = {{PATH}, a Program Transformation System for {H}askell},
 year = {2002},
 isbn = {0-493-60483-9},
 order_no = {AAI3046238},
 school = {Yale University},
 address = {New Haven, CT, USA},
 url = "http://www.cs.yale.edu/publications/techreports/tr1229.pdf"
}

@article{Harel:1980,
 author = {Harel, D.},
 title = {On folk theorems},
 journal = "{C}. ACM",
 volume = 23,
 number = 7,
 year = 1980,
 pages = {379--389},
 doi = {http://doi.acm.org/10.1145/358886.358892},
 publisher = {ACM},
}

@article{DBLP:journals/toplas/Sangiorgi09,
  author    = {Davide Sangiorgi},
  title     = {On the origins of bisimulation and coinduction},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {31},
  number    = {4},
  year      = {2009},
  ee        = {http://doi.acm.org/10.1145/1516507.1516510},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Bekic:1969,
 author = {Beki\'{c}, H.},
 title = {Definable Operation in General Algebras, and the Theory of Automata and Flowcharts},
 booktitle = {Programming Languages and Their Definition - Hans Beki\'{c} (1936-1982)},
 year = {1984},
 pages = {30--55},
 publisher = {Springer-Verlag},
}

@inproceedings{SPJ-JL:1991,
 author = {Peyton Jones, S. and Launchbury, J.},
 title = {Unboxed values as first class citizens in a non-strict functional language},
 booktitle = {Proceedings of the 5th {ACM} Conference on Functional programming languages and computer architecture},
 year = {1991},
 pages = {636--666},
 publisher = {Springer-Verlag},
}

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

@article{BurstallDarlington:1977,
 author = {R. M. Burstall and J. Darlington},
 title = {A Transformation System for Developing Recursive Programs},
 journal = "{J}. {ACM}",
 volume = {24},
 number = {1},
 year = {1977},
 pages = {44--67},
 doi = {http://doi.acm.org/10.1145/321992.321996},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{DBLP:conf/icfp/WandV04,
  author    = {M. Wand and
               D. Vaillancourt},
  title     = {Relating models of backtracking},
  booktitle = {ICFP},
  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}
}

@proceedings{DBLP:conf/icfp/2004,
  editor    = {C. Okasaki and
               K. Fisher},
  title     = {Proceedings of the Ninth ACM SIGPLAN International Conference
               on Functional Programming, ICFP 2004, Snow Bird, UT, USA,
               September 19-21, 2004},
  booktitle = {ICFP},
  publisher = {ACM},
  year      = {2004},
  isbn      = {1-58113-905-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/ngc/DanvyGR01,
  author    = {O. Danvy and
               B. Grobauer and
               M. Rhiger},
  title     = {A Unifying Approach to Goal-directed Evaluation},
  journal   = {New Generation Comput.},
  volume    = {20},
  number    = {1},
  year      = {2001},
  pages     = {53-74},
  ee        = {https://doi.org/10.1007/BF03037259},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  ee        = {https://doi.org/10.1017/S0956796810000122},
@article{DBLP:journals/jfp/HuttonJG10,
  author    = {G. Hutton and
               M. Jaskelioff and
               A. Gill},
  title     = {Factorising folds for faster functions},
  journal = "{J}ournal of {F}unctional {P}rogramming",
  volume    = {20},
  number    = {3-4},
  year      = {2010},
  pages     = {353-373},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

% 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/lics/SimpsonP00,
  author    = {A. K. Simpson and
               G. D. Plotkin},
  title     = {Complete Axioms for Categorical Fixed-Point Operators},
  booktitle = {LICS},
  year      = {2000},
  pages     = {30-41},
  ee        = {http://www.computer.org/proceedings/lics/0725/07250030abs.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@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},
  series    = {Prentice-Hall international series in computer science},
  year      = {1980},
  pages     = {I-XV, 1-505},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/icalp/Reynolds74,
  author    = {J. C. Reynolds},
  title     = {On the Relation between Direct and Continuation Semantics},
  booktitle = {ICALP},
  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 = {ICALP},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {14},
  year      = {1974},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

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

@inproceedings{DBLP:conf/flops/Danvy99,
  author    = {O. Danvy},
  title     = {An Extensional Characterization of Lambda-Lifting and Lambda-Dropping},
  booktitle = {Fuji International Symposium on Functional and Logic Programming},
  year      = {1999},
  pages     = {241-250},
  ee        = {https://doi.org/10.1007/10705424_16},
  crossref  = {DBLP:conf/flops/1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/flops/1999,
  editor    = {A. Middeldorp and
               T. Sato},
  title     = {Functional and Logic Programming, 4th Fuji International
               Symposium, FLOPS'99, Tsukuba, Japan, November 11-13, 1999,
               Proceedings},
  booktitle = {FLOPS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1722},
  year      = {1999},
  isbn      = {3-540-66677-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  note =         {(Special issue of selected papers from 6'th
%                  Conference on Lisp and Functional Programming.)}
@Article{wadler92:_comprehending_monads,
  author =       {P. Wadler},
  title =        {Comprehending monads},
  journal =      {MSCS},
  year =         {1992},
  volume =       {2},
  pages =        {461--493},
}
