@inproceedings(DomainCoq,
 author       = "N. Benton and A. Kennedy and C. Varming",
 year         = "2009",
 title        = "Some Domain Theory and Denotational Semantics in Coq",
 editor       = "S. Berghofer and T. Nipkow and C. Urban and M. Wenzel",
 booktitle    = "Proc. of 22nd Int. Conf. on Theorem Proving in Higher-Order Logics, TPHOLs 2009",
 series       = "LNCS",
 volume       = "5674",
 publisher    = "Springer",
 pages        = "115--130",
 doi          = "10.1007/978-3-642-03359-9\_10",
)
@article(Cap:genrct,
 author       = "V. Capretta",
 year         = "2005",
 title        = "General recursion via coinductive types",
 journal      = "Logical Methods in Comput. Sci.",
 volume       = "1",
 number       = "2",
 doi          = "10.2168/LMCS-1(2:1)2005",
)
@inproceedings(CM:synmds,
 author       = "P. Cenciarelli and E. Moggi",
 year         = "1993",
 title        = "A syntactic approach to modularity in denotational semantics",
 booktitle    = "Proc. of 5th Biennial Meeting on Category Theory and Computer Science, CTCS 1993",
)
@article(HJS:gentsc,
 author       = "I. Hasuo and B. Jacobs and A. Sokolova",
 year         = "2007",
 title        = "Generic trace semantics via coinduction",
 journal      = "Logical Methods in Comput. Sci.",
 volume       = "3",
 number       = "4",
 doi          = "10.2168/LMCS-3(4:11)2007",
)
@inproceedings(nonterm,
 author       = "K. Nakata and T. Uustalu",
 year         = "2009",
 title        = "Trace-based coinductive operational semantics for While: big-step and small-step, relational and functional styles",
 editor       = "S. Berghofer and T. Nipkow and C. Urban and M. Wenzel",
 booktitle    = "Proc. of 22nd Int. Conf. on Theorem Proving in Higher-Order Logics, TPHOLs 2009",
 series       = "LNCS",
 volume       = "5674",
 publisher    = "Springer",
 pages        = "375--390",
 doi          = "10.1007/978-3-642-03359-9\_26",
)
@inproceedings(interact,
 author       = "K. Nakata and T. Uustalu",
 year         = "2010",
 title        = "Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction",
 editor       = "L. Aceto and P. Sobocinski",
 booktitle    = "Proc. of 7th Workshop on Structural Operational Semantics, SOS 2010",
 series       = "Electron. Proc. in Theor. Comput. Sci.",
 volume       = "32",
 pages        = "57--75",
 doi          = "10.4204/EPTCS.32.5",
)
@inproceedings(DomainKahn,
 author       = "C. Paulin-Mohring",
 year         = "2009",
 title        = "A constructive denotational semantics for Kahn networks in Coq",
 editor       = "Y. Bertot and G. Huet and J.-J. L\'{e}vy and G. Plotkin",
 booktitle    = "From Semantics to Computer Science -- Essays in Honour of Gilles Kahn",
 publisher    = "Cambridge University Press",
 pages        = "383--414",
 doi          = "10.1017/CBO9780511770524.018",
)
@unpublished(Plo:dom,
 author       = "G. D. Plotkin",
 year         = "1983",
 title        = "Domains (``Pisa Notes'')",
 note         = "Unpublished notes",
)
@article(Rut:notcwb,
 author       = "J. Rutten",
 year         = "1999",
 title        = "A note on coinduction and weak bisimilarity for While programs",
 journal      = "Theor.\ Inform.\ and Appl.",
 volume       = "33",
 number       = "4--5",
 pages        = "393--400",
 doi          = "10.1051/ita:1999125",
)
@phdthesis(WeijlandPhD,
 author       = "W. P. Weijland",
 year         = "1989",
 title        = "Synchrony and Asynchrony in Process Algebra",
 school       = "University of Amsterdam",
)