1: \begin{thebibliography}{}
2:
3: \bibitem[Abramsky and Jung, 1994]{AJ:domains}
4: Abramsky, S. and Jung, A. (1994).
5: \newblock Domain theory.
6: \newblock In Abramsky, S., Gabbay, D.~M., and Maibaum, T. S.~E., editors, {\em
7: Handbook of Logic in Computer Science}, volume~3, pages 1--168. Oxford
8: University Press.
9:
10: \bibitem[Adamek et~al., 1990]{AHS}
11: Adamek, J., Herrlich, H., and Strecker, G. (1990).
12: \newblock {\em Abstract and Concrete Categories}.
13: \newblock Wiley, New York.
14:
15: \bibitem[Alimohamed, 1995]{Ali95}
16: Alimohamed, M. (1995).
17: \newblock A characterization of lambda definability in categorical models of
18: implicit polymorphism.
19: \newblock {\em Theoretical Computer Science}, 146(1--2):5--23.
20:
21: \bibitem[Ambler, 1991]{SJA:thesis}
22: Ambler, S.~J. (1991).
23: \newblock {\em First Order Linear Logic in Symmetric Monoidal Closed
24: Categories}.
25: \newblock PhD thesis, University of Edinburgh.
26:
27: \bibitem[Appelgate, 1965]{App65}
28: Appelgate, H. (1965).
29: \newblock {\em Acyclic models and resolvent functors}.
30: \newblock PhD thesis, Columbia University.
31:
32: \bibitem[Barr, 1998]{Barr98}
33: Barr, M. (1998).
34: \newblock The separated extensional {C}hu category.
35: \newblock {\em Theory and Applications of Categories}, 4(6):137--147.
36:
37: \bibitem[Beck, 1969]{Beck:distr}
38: Beck, J. (1969).
39: \newblock Distributive laws.
40: \newblock In {\em Seminar on Triples and Categorical Homology Theory}, pages
41: 119--140. Springer-Verlag LNM 80.
42:
43: \bibitem[Bourbaki, 1969]{Bourbaki:int:IX}
44: Bourbaki, N. (1969).
45: \newblock {\em Int{\'e}gration}, volume~IX.
46: \newblock Diffusion CCLS.
47:
48: \bibitem[Carboni et~al., 1990]{CKW90}
49: Carboni, A., Kelly, G.~M., and Wood, R.~J. (1990).
50: \newblock A 2-categorical approach to change of base and geometric morphisms
51: {I}.
52: \newblock Report 90-1, Department of Pure Mathematics, University of Sydney.
53:
54: \bibitem[Crole and Pitts, 1992]{Pitts92}
55: Crole, R. and Pitts, A. (1992).
56: \newblock New foundations for fixpoint computations: Fix-hyperdoctrines and the
57: fix-logic.
58: \newblock {\em Information and Computation}, 98:171--210.
59:
60: \bibitem[de~Vink and Rutten, 1999]{dVR:proba:bisim}
61: de~Vink, E.~P. and Rutten, J. J. M.~M. (1999).
62: \newblock Bisimulation for probabilistic transition systems: A coalgebraic
63: approach.
64: \newblock {\em Theoretical Computer Science}, 221(1--2):271--293.
65:
66: \bibitem[Desharnais et~al., 2002]{DEP:markov:bisim}
67: Desharnais, J., Edalat, A., and Panangaden, P. (2002).
68: \newblock Bisimulation for labelled {M}arkov processes.
69: \newblock {\em Information and Computation}, 179(2):163--193.
70:
71: \bibitem[Eilenberg and Kelly, 1966]{EK:closed:cat}
72: Eilenberg, S. and Kelly, G.~M. (1966).
73: \newblock Closed categories.
74: \newblock In {\em Proceedings of the Conference on Categorical Algebra at La
75: Jolla}, pages 421--562. Springer-Verlag.
76:
77: \bibitem[Escard{\'o} and Heckmann, 2002]{EH:topfun}
78: Escard{\'o}, M. and Heckmann, R. (2001--2002).
79: \newblock Topologies on spaces of continuous functions.
80: \newblock {\em Topology Proceedings}, 26(2):545--564.
81:
82: \bibitem[Escard{\'o} et~al., 2004]{ELS:CCC:Top}
83: Escard{\'o}, M., Lawson, J., and Simpson, A. (2004).
84: \newblock Comparing cartesian closed categories of (core) compactly generated
85: spaces.
86: \newblock {\em Topology and Its Applications}, 143(1--3):105--146.
87:
88: \bibitem[Fiore and Simpson, 1999]{FS99}
89: Fiore, M. and Simpson, A. (1999).
90: \newblock Lambda definability with sums via {G}rothendieck logical relations.
91: \newblock In {\em Proceedings of the 4th International Conference on Typed
92: Lambda-Calculi and Applications (TLCA'99)}, pages 147--161. Springer-Verlag
93: LNCS 1581.
94:
95: \bibitem[Freyd and Kelly, 1972]{FK:cont}
96: Freyd, P.~J. and Kelly, G.~M. (1972).
97: \newblock Categories of continuous functors~i.
98: \newblock {\em Journal of Pure and Applied Algebra}, 2(3):169--191.
99:
100: \bibitem[Gierz et~al., 1980]{GHKLMS:compendium}
101: Gierz, G., Hofmann, K.~H., Keimel, K., Lawson, J.~D., Mislove, M., and Scott,
102: D.~S. (1980).
103: \newblock {\em A Compendium of Continuous Lattices}.
104: \newblock Springer Verlag.
105:
106: \bibitem[Gierz et~al., 2003]{GHKLMS:contlatt}
107: Gierz, G., Hofmann, K.~H., Keimel, K., Lawson, J.~D., Mislove, M., and Scott,
108: D.~S. (2003).
109: \newblock Continuous lattices and domains.
110: \newblock In {\em Encyclopedia of Mathematics and its Applications}, volume~93.
111: Cambridge University Press.
112:
113: \bibitem[Giry, 1981]{Giry:proba}
114: Giry, M. (1981).
115: \newblock A categorical approach to probability theory.
116: \newblock In Banaschewski, B., editor, {\em Categorical Aspects of Topology and
117: Analysis}, pages 68--85. Springer Verlag LNM 915.
118:
119: \bibitem[Goubault-Larrecq, 2005]{JGL:val:ext}
120: Goubault-Larrecq, J. (2005).
121: \newblock Extensions of valuations.
122: \newblock {\em Mathematical Structures in Computer Science}, 15(2):271--297.
123: \newblock An early version is available as LSV Research Report LSV-02-17, Nov.
124: 2002.
125:
126: \bibitem[{Goubault-Larrecq} and Goubault, 2003]{GG01}
127: {Goubault-Larrecq}, J. and Goubault, E. (2003).
128: \newblock On the geometry of intuitionistic {S4} proofs.
129: \newblock {\em Homology, Homotopy and Applications}, 5(2):137--209.
130:
131: \bibitem[Goubault-Larrecq et~al., 2002]{GLN02b}
132: Goubault-Larrecq, J., Lasota, S., and Nowak, D. (2002).
133: \newblock Logical relations for monadic types.
134: \newblock In {\em Proceedings of the 16th International Workshop on Computer
135: Science Logic (CSL'02)}. Springer-Verlag LNCS 2471.
136:
137: \bibitem[Heckmann, 1990]{Heckmann:PhD}
138: Heckmann, R. (1990).
139: \newblock {\em Power Domain Constructions (Potenzbereich-Konstruktionen)}.
140: \newblock PhD thesis, Universit{\"a}t des Saarlandes.
141:
142: \bibitem[Hermida, 1993]{Her93}
143: Hermida, C.~A. (1993).
144: \newblock {\em Fibrations, logical predicates and indeterminates}.
145: \newblock PhD thesis, University of Edinburgh, Department of Computer Science.
146: \newblock Also published as ECS-LFCS-93-277.
147:
148: \bibitem[Honsell and Sannella, 2002]{HS99}
149: Honsell, F. and Sannella, D. (2002).
150: \newblock Prelogical relations.
151: \newblock {\em Information and Computation}, 178:23--43.
152:
153: \bibitem[Johnstone, 1975]{John75}
154: Johnstone, P. (1975).
155: \newblock Adjoint lifting theorems for categories of algebras.
156: \newblock {\em Bulletin of the London Mathematical Society}, 7:294--297.
157:
158: \bibitem[Jones, 1990]{Jones:proba}
159: Jones, C. (1990).
160: \newblock {\em Probabilistic Non-Determinism}.
161: \newblock PhD thesis, University of Edinburgh.
162: \newblock Technical Report ECS-LFCS-90-105.
163:
164: \bibitem[Jung, 1990]{Jung:CCC}
165: Jung, A. (1990).
166: \newblock The classification of continuous domains.
167: \newblock In {\em Proc. IEEE Symp.\ Logic in Computer Science (LICS'90)}, pages
168: 35--40. IEEE Computer Society Press.
169:
170: \bibitem[Jung and Tiuryn, 1993]{JT93}
171: Jung, A. and Tiuryn, J. (1993).
172: \newblock A new characterization of lambda definability.
173: \newblock In {\em Proceedings of the 1st International Conference on Typed
174: Lambda-Calculi and Applications (TLCA'93)}, pages 245--257. Springer Verlag
175: LNCS 664.
176:
177: \bibitem[Kinoshita and Power, 1999]{KP99}
178: Kinoshita, Y. and Power, J. (1999).
179: \newblock Data-refinement for call-by-value programming languages.
180: \newblock In {\em Computer Science Logic, 13th International Workshop, CSL '99,
181: 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999,
182: Proceedings}, pages 562--576.
183:
184: \bibitem[Larsen and Skou, 1991]{LS:proba}
185: Larsen, K.~G. and Skou, A. (1991).
186: \newblock Bisimulation through probabilistic testing.
187: \newblock {\em Information and Computation}, 94:1--28.
188:
189: \bibitem[Lawvere, 1973]{Lawvere:metric}
190: Lawvere, F.~W. (1973).
191: \newblock Metric spaces, generalized logic, and closed categories.
192: \newblock {\em Rendiconti del Seminario Matematico e Fisico di Milano},
193: 43:135--166.
194:
195: \bibitem[Lazi{\'c} and Nowak, 2000]{LN00}
196: Lazi{\'c}, R. and Nowak, D. (2000).
197: \newblock A unifying approach to data-independence.
198: \newblock In {\em Proceedings of the 11th Internal Conference on Concurrency
199: Theory (CONCUR'2000)}, pages 581--595. Springer-Verlag LNCS 1877.
200:
201: \bibitem[Ma and Reynolds, 1992]{MR92}
202: Ma, Q. and Reynolds, J.~C. (1992).
203: \newblock Types, abstraction, and parametric polymorphism, part~2.
204: \newblock In {\em 7th International Conference on Mathematical Foundations of
205: Programming Semantics (MFPS'91)}, pages 1--40. Springer-Verlag LNCS 598.
206:
207: \bibitem[Mac~Lane, 1971]{McLane:cat:math}
208: Mac~Lane, S. (1971).
209: \newblock {\em Categories for the Working Mathematician}, volume~5 of {\em
210: Graduate Texts in Mathematics}.
211: \newblock Springer-Verlag.
212:
213: \bibitem[Mitchell, 1996]{Mit96}
214: Mitchell, J.~C. (1996).
215: \newblock {\em Foundations for Programming Languages}.
216: \newblock MIT Press.
217:
218: \bibitem[Mitchell and Scedrov, 1993]{MS93}
219: Mitchell, J.~C. and Scedrov, A. (1993).
220: \newblock Notes on sconing and relators.
221: \newblock In B{\"o}rger, E., J{\"a}ger, G., Kleine~B{\"u}ning, H., Martini, S.,
222: and Richter, M.~M., editors, {\em Proceedings of the 6th International
223: Workshop on Computer Science Logic (CSL'92)}, pages 352--378. Springer Verlag
224: LNCS 702.
225:
226: \bibitem[Moggi, 1991]{Mog91}
227: Moggi, E. (1991).
228: \newblock Notions of computation and monads.
229: \newblock {\em Information and Computation}, 93:55--92.
230:
231: \bibitem[Moggi, 1995]{Mog95}
232: Moggi, E. (1995).
233: \newblock A semantics for evaluation logic.
234: \newblock {\em Fundam. Inform}, 22(1/2):117--152.
235:
236: \bibitem[Pitts and Stark, 1993]{pitts/stark:obsphown}
237: Pitts, A. and Stark, I. (1993).
238: \newblock Observable properties of higher order functions that dynamically
239: create local names, or: What's {\em new}?
240: \newblock In Borzyszkowski, A. and Soko{\l}owski, S., editors, {\em Proceedings
241: of the 18th International Symposium on Mathematical Foundations of Computer
242: Science (MFCS'93)}, pages 122--141. Springer-Verlag LNCS 711.
243:
244: \bibitem[Pitts, 1991]{Pit91}
245: Pitts, A.~M. (1991).
246: \newblock Evaluation logic.
247: \newblock In Birtwistle, G., editor, {\em IVth Higher Order Workshop, {Banff}
248: 1990}, Workshops in Computing, pages 162--189. Springer-Verlag, Berlin.
249:
250: \bibitem[Pitts, 1996]{Pit96}
251: Pitts, A.~M. (1996).
252: \newblock Relational properties of domains.
253: \newblock {\em Information and Computation}, 127(2):66--90.
254:
255: \bibitem[Plotkin et~al., 2000]{PPST00}
256: Plotkin, G., Power, J., Sannella, D., and Tennent, R. (2000).
257: \newblock Lax logical relations.
258: \newblock In {\em Proceedings of the 7th International Colloquium on Automata,
259: Languages and Programming (ICALP'2000)}, pages 85--102. Springer Verlag LNCS
260: 1853.
261:
262: \bibitem[Plotkin, 1980]{Plo80}
263: Plotkin, G.~D. (1980).
264: \newblock Lambda-definability in the full type hierarchy.
265: \newblock In Seldin, J. and Hindley, J., editors, {\em To H. B. Curry: Essays
266: on Combinatory Logic, Lambda Calculus and Formalism}, pages 363--373.
267: Academic Press.
268:
269: \bibitem[Power and Tanaka, 2000]{PT00}
270: Power, J. and Tanaka, M. (2000).
271: \newblock Axiomatics for data refinement in call by value programming
272: languages.
273:
274: \bibitem[Power and Watanabe, 2002]{PW02}
275: Power, J. and Watanabe, H. (2002).
276: \newblock Combining a monad and a comonad.
277: \newblock {\em Theoretical Computer Science}, 280(1--2):137--162.
278:
279: \bibitem[Prawitz, 1965]{Prawitz:natdeduc}
280: Prawitz, D. (1965).
281: \newblock {\em Natural Deduction, A Proof-Theoretical Study}.
282: \newblock Almqvist and Wiskell, Stockholm.
283:
284: \bibitem[Ramsey and Pfeffer, 2002]{RP02}
285: Ramsey, N. and Pfeffer, A. (2002).
286: \newblock Stochastic lambda calculus and monads of probability distributions.
287: \newblock In {\em Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium
288: on Principles of Programming Languages (POPL'02)}, pages 154--165.
289:
290: \bibitem[Reynolds, 1983]{Rey83}
291: Reynolds, J.~C. (1983).
292: \newblock Types, abstraction and parametric polymorphism.
293: \newblock In {\em Proceedings of the 9th World Computer Congress (IFIP'83)},
294: pages 513--523. North-Holland.
295:
296: \bibitem[Rutten, 1998]{Rut98}
297: Rutten, J. (1998).
298: \newblock Relators and metric bisimulations.
299: \newblock In {\em Proceedings of the 1th Workshop on Coalgebraic Methods in
300: Computer Science (CMCS '98)}, volume~11 of {\em ENTCS}, pages 1--7. Elsevier
301: Science.
302:
303: \bibitem[Stark, 1996]{Sta96}
304: Stark, I. (1996).
305: \newblock Categorical models for local names.
306: \newblock {\em Lisp and Symbolic Computation}, 9(1):77--107.
307:
308: \bibitem[Stark, 1998]{stark:namerp-fi}
309: Stark, I. (1998).
310: \newblock Names, equations, relations: Practical ways to reason about {\em
311: new}.
312: \newblock {\em Fundamenta Informaticae}, 33(4):369--396.
313:
314: \bibitem[Statman, 1985]{Sta85}
315: Statman, R. (1985).
316: \newblock Logical relations and the typed $\lambda$-calculus.
317: \newblock {\em Information and Control}, 65(2--3):85--97.
318:
319: \bibitem[Street, 1972]{Street:monads}
320: Street, R. (1972).
321: \newblock The formal theory of monads.
322: \newblock {\em Journal of Pure and Applied Algebra}, 2:149--168.
323:
324: \bibitem[Turi, 1996]{Turi96}
325: Turi, D. (1996).
326: \newblock {\em Functorial Operational Semantics and its Denotational Dual}.
327: \newblock PhD thesis, Free University, Amsterdam.
328:
329: \bibitem[Wadler, 1992]{Wadler:comprehending}
330: Wadler, P. (1992).
331: \newblock Comprehending monads.
332: \newblock {\em Mathematical Structures in Computer Science}, 2:461--493.
333:
334: \bibitem[Worrell, 2000]{Worrell:PhD}
335: Worrell, J. (2000).
336: \newblock {\em On Coalgebras and Final Semantics}.
337: \newblock PhD thesis, Keble College, Oxford University Computing Laboratory.
338:
339: \bibitem[Zhang, 2005]{Zha:05}
340: Zhang, Y. (2005).
341: \newblock {\em Relations logiques cryptographiques --- Qu'est-ce que
342: l'{\'e}quivalence contextuelle des protocoles cryptographiques et comment la
343: prouver~?}
344: \newblock PhD thesis, Laboratoire Sp{\'e}cification et V{\'e}rification, Ecole
345: Normale Sup{\'e}rieure de Cachan.
346:
347: \bibitem[Zhang and Nowak, 2003]{ZN:logrelnames}
348: Zhang, Y. and Nowak, D. (2003).
349: \newblock Logical relation for dynamic name creation.
350: \newblock In {\em Proceedings of the 17th International Workshop on Computer
351: Science Logic (CSL'03)}, pages 575--588. Springer-Verlag LNCS 2803.
352:
353: \end{thebibliography}
354: