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