J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

J. Andreoli, Focussing and proof construction, Annals of Pure and Applied Logic, vol.107, issue.1-3, pp.131-163, 2001.
DOI : 10.1016/S0168-0072(00)00032-4
URL : http://doi.org/10.1016/s0168-0072(00)00032-4

D. Baelde, A linear approach to the proof-theory of least and greatest fixed points, 2008.

D. Baelde, Least and greatest fixed points in linear logic, 2009.

D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu, The Bedwyr System for Model Checking over Syntactic Expressions, 21th Conference on Automated Deduction (CADE), number 4603 in LNAI, pp.391-397, 2007.
DOI : 10.1007/978-3-540-73595-3_28

D. Baelde and D. Miller, Least and greatest fixed points in linear logic, International Conference on Logic for Programming and Automated Reasoning (LPAR), pp.92-106, 2007.

D. Baelde, D. Miller, and Z. Snow, Focused Inductive Theorem Proving, 2010.
DOI : 10.1007/978-3-642-14203-1_24
URL : https://hal.archives-ouvertes.fr/hal-00772592

J. Brotherston and A. Simpson, Complete Sequent Calculi for Induction and Infinite Descent, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.51-62, 2007.
DOI : 10.1109/LICS.2007.16

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992.
DOI : 10.1007/3-540-54487-9_58

J. Girard, A fixpoint theorem in linear logic. A posting to linear@cs, 1992.

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar, Decision problems for propositional linear logic, Annals of Pure and Applied Logic, vol.56, issue.1-3, pp.239-311, 1992.
DOI : 10.1016/0168-0072(92)90075-B

R. Mcdowell and D. Miller, Reasoning with higher-order abstract syntax in a logical framework, ACM Transactions on Computational Logic, vol.3, issue.1, pp.80-136, 2002.
DOI : 10.1145/504077.504080

D. Miller, Finding unity in computational logic, ACM-BCS-Visions Conference, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00772557

D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W

D. Miller and V. Nigam, Incorporating Tables into Proofs, CSL 2007: Computer Science Logic, pp.466-480, 2007.
DOI : 10.1007/978-3-540-74915-8_35

D. Miller and A. Saurin, A Game Semantics for Proof Search: Preliminary Results, Proceedings of the Mathematical Foundations of Programming Semantics (MFPS05), number 155 in Electronic Notes in Theoretical Computer Science, pp.543-563, 2006.
DOI : 10.1016/j.entcs.2005.11.072
URL : https://hal.archives-ouvertes.fr/hal-00527881

V. Nigam and D. Miller, Algorithmic specifications in linear logic with subexponentials, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, PPDP '09, pp.129-140, 2009.
DOI : 10.1145/1599410.1599427

L. Santocanale, A calculus of circular proofs and its categorical semantics, Proceedings of Foundations of Software Science and Computation Structures (FOSSACS02), number 2303 in LNCS, pp.357-371
URL : https://hal.archives-ouvertes.fr/hal-01261170

P. Schroeder-heister, Rules of definitional reflection, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.222-232, 1993.
DOI : 10.1109/LICS.1993.287585

A. Tiu, A Logical Framework for Reasoning about Logical Specifications, 2004.

. References, V. Kountouriotis, C. Nomikos, and P. Rondogiannis, Well-Founded Semantics for Boolean Grammars, Information and Computation, vol.207, issue.9, pp.945-967, 2009.

A. Okhotin, Boolean grammars, Information and Computation, vol.194, issue.1, pp.19-48, 2004.
DOI : 10.1016/j.ic.2004.03.006
URL : http://doi.org/10.1016/j.ic.2004.03.006

P. Rondogiannis, W. Wadge, and W. , Minimum model semantics for logic programs with negation-as-failure, ACM Transactions on Computational Logic, vol.6, issue.2, pp.441-467, 2005.
DOI : 10.1145/1055686.1055694

A. Van-gelder, K. Ross, A. Schlipf, J. , and S. , The well-founded semantics for general logic programs, Journal of the ACM, vol.38, issue.3, pp.620-650, 1991.
DOI : 10.1145/116825.116838

]. P. America and J. J. Rutten, Solving reflexive domain equations in a category of complete metric spaces, Journal of Computer and System Sciences, vol.39, issue.3, pp.343-375, 1989.
DOI : 10.1016/0022-0000(89)90027-5

A. W. Appel and D. Mcallester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems, vol.23, issue.5, pp.657-683, 2001.
DOI : 10.1145/504709.504712

A. W. Appel, P. Mellì-es, C. D. Richards, and J. Vouillon, A very modal model of a modern, major, general type system, Proceedings of POPL, pp.109-122, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00150978

L. Birkedal, K. Støvring, and J. Thamsborg, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, Proceedings of FOSSACS, pp.456-470, 2009.
DOI : 10.1137/0211062

M. Escardó, A metric model of PCF Available at the author's web page, 1999.

R. Hinze, Functional pearl: streams and unique fixed points, Proceedings of ICFP, pp.189-200, 2008.
DOI : 10.1007/978-3-540-70594-9_1

N. Krishnaswami, L. Birkedal, and J. Aldrich, Verifying event-driven programs using ramified frame properties, Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '10, pp.63-76, 2010.
DOI : 10.1145/1708016.1708025

H. Nakano, A modality for recursion, Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pp.255-266, 2000.
DOI : 10.1109/LICS.2000.855774

F. Pottier, A typed store-passing translation for general references, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01081187

N. Zeilberger, The Logical Basis of Evaluation Order and Pattern-Matching, 2009.

]. A. Ahmed, M. Fluet, and G. Morrisett, L3: A linear language with locations, Fundam. Inf, vol.77, issue.4, pp.397-449, 2007.

P. America and J. J. Rutten, Solving reflexive domain equations in a category of complete metric spaces, Journal of Computer and System Sciences, vol.39, issue.3, pp.343-375, 1989.
DOI : 10.1016/0022-0000(89)90027-5

B. Biering, L. Birkedal, and N. Torp-smith, BI-hyperdoctrines, higher-order separation logic, and abstraction, ACM Transactions on Programming Languages and Systems, vol.29, issue.5, 2007.
DOI : 10.1145/1275497.1275499
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.138.4297

L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg et al., Step-indexed Kripke models over recursive worlds, 2010.
DOI : 10.1145/1925844.1926401
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.190.2081

L. Birkedal, K. Støvring, and J. Thamsborg, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, FOSSACS, pp.456-470, 2009.
DOI : 10.1137/0211062

L. Birkedal, N. Torp-smith, and H. Yang, Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages, Logical Methods in Computer Science, vol.2, issue.5, 2006.
DOI : 10.2168/LMCS-2(5:1)2006

A. Charguéraud and F. Pottier, Functional translation of a calculus of capabilities, ICFP, pp.213-224, 2008.

K. Crary, D. Walker, and G. Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.262-275, 1999.
DOI : 10.1145/292540.292564

F. Pottier, Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.331-340, 2008.
DOI : 10.1109/LICS.2008.16

F. Pottier, Generalizing the higher-order frame and anti-frame rules. Unpublished, 2009.

J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang, Nested Hoare Triples and Frame Rules for Higher-Order Store, CSL, pp.440-454, 2009.
DOI : 10.1142/6284

J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus, A Semantic Foundation for Hidden State, FOSSACS, pp.2-16, 2010.
DOI : 10.1007/978-3-642-12032-9_2

M. B. Smyth, References [1] G. Fontaine, Continuous fragment of the µ?calculus, Topology. In Handbook of Logic in Computer Science Lecture Notes in Computer Science, vol.1, issue.5213, pp.139-153, 1992.

A. Arnold and D. Niwi´nskiniwi´nski, Rudiments of µ?Calculus, Studies in Logic, vol.146, 2001.

J. Bradfield and C. Stirling, Modal mu?calculi The Handbook of Modal Logic pp, pp.721-756, 2006.

P. Aczel, An Introduction to Inductive Definitions, Handbook of Mathematical Logic of Studies in Logic and the Foundations of Mathematics, chapter, pp.739-782, 1977.
DOI : 10.1016/S0049-237X(08)71120-0

Y. Bertot and V. Komendantsky, Fixed point semantics and partial recursion in Coq, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.89-96, 2008.
DOI : 10.1145/1389449.1389461
URL : https://hal.archives-ouvertes.fr/inria-00190975

N. Bourbaki, Théorie des ensembles : Fascicule de résultats, 1939.

S. Burris and H. Sankappanavar, A Course in Universal Algebra. Number 78 in Graduate Texts in Mathematics, 1981.

P. Cousot and R. Cousot, Constructive versions of Tarski???s fixed point theorems, Pacific Journal of Mathematics, vol.82, issue.1, pp.43-57, 1979.
DOI : 10.2140/pjm.1979.82.43

S. Lang, Algebra, Revised Third Edition. Graduate Texts in Mathematics, 2002.

X. Leroy and H. Grall, Coinductive big-step operational semantics, Information and Computation, vol.207, issue.2, pp.284-304, 2009.
DOI : 10.1016/j.ic.2007.12.004
URL : https://hal.archives-ouvertes.fr/inria-00309010

G. Markowsky, Chain-complete posets and directed sets with applications, Algebra Universalis, vol.5, issue.1, pp.53-68, 1976.
DOI : 10.1007/BF02485815

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-309, 1955.
DOI : 10.2140/pjm.1955.5.285

]. S. References-[-abr90 and . Abramsky, The lazy ? -calculus, Research topics in Functional Programming, pp.65-117

S. Abramsky, A domain equation for bisimulation. Information and Computation, 1991.

J. Friso-groote and F. Vaandrager, Structured operational semantics and bisimulation as a congruence, Information and Computation, vol.100, issue.2, pp.202-260, 1992.
DOI : 10.1016/0890-5401(92)90013-6

D. Howe, Proving Congruence of Bisimulation in Functional Programming Languages, Information and Computation, vol.124, issue.2, 1996.
DOI : 10.1006/inco.1996.0008

S. Lassen, Relational Reasoning about Functions and Nondeterminism, 1998.

P. Levy, Infinitary Howe's Method, Proc., 8th Intl. Workshop on Coalgebraic Methods in Comp. Sci., Vienna, 2006.
DOI : 10.1016/j.entcs.2006.06.006

P. Blain, L. , and K. Weldemariam, Exploratory functions on nondeterministic strategies , up to lower bisimilarity, Electr. Notes Theor. Comput. Sci, vol.249, pp.357-375, 2009.

R. Milner, Communication and Concurrency, 1989.

A. Roscoe, Seeing beyond divergence. presented at BCS FACS meeting " 25 Years of CSP, 2004.
DOI : 10.1007/11423348_2
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.1076

D. Turi and J. J. Rutten, On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces, Mathematical Structures in Computer Science, vol.8, issue.5, pp.481-540, 1998.
DOI : 10.1017/S0960129598002588

G. Winskel and M. Nielsen, Models for concurrency, Handbook of Logic in Computer Science, 1995.

L. De-alfaro and R. Majumdar, Quantitative solution of omega-regular games, Journal of Computer and System Sciences, vol.68, issue.2, pp.374-397, 2004.
DOI : 10.1016/j.jcss.2003.07.009

E. A. Emerson and C. S. Jutla, Tree automata, mu-calculus and determinacy, [1991] Proceedings 32nd Annual Symposium of Foundations of Computer Science, pp.368-377, 1991.
DOI : 10.1109/SFCS.1991.185392

D. Fischer, E. Gradel, and L. Kaiser, Model Checking Games for the Quantitative ??-Calculus, Theory of Computing Systems, 2009.
DOI : 10.1007/s00224-009-9201-y
URL : https://hal.archives-ouvertes.fr/hal-00255805

M. Huth and M. Kwiatkowska, Quantitative analysis and model checking, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.
DOI : 10.1109/LICS.1997.614940

D. Janin and I. Walukiewicz, On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic, Lecture Notes in Computer Science, vol.1119, pp.263-277, 1996.
DOI : 10.1007/3-540-61604-7_60

D. Kozen, Results on the propositional mu-calculus, Theoretical Computer Science, pp.333-354, 1983.

D. A. Martin, The determinacy of Blackwell games, Journal of Symbolic Logic, pp.1565-1581, 1998.
DOI : 10.1007/BF02801569

A. Mciver and C. Morgan, Results on the quantitative mu-calculus qmu. CoRR, cs, p.309024, 2003.

A. Mciver and C. Morgan, ??, ACM Transactions on Computational Logic, vol.8, issue.1, p.3, 2007.
DOI : 10.1145/1182613.1182616

M. Mio, Extended version available at

C. Morgan and A. Mciver, A probabilistic temporal calculus based on expectations, Proc. Formal Methods, 1997.

R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, 1995.

C. Stirling, Modal and temporal logics for processes, Texts in Computer Science), 2001.
DOI : 10.1007/3-540-60915-6_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.9078

T. Studer, On the Proof Theory of the Modal mu-Calculus, Studia Logica, 2007.
DOI : 10.1007/s11225-008-9133-6

Z. Ariola and S. Blom, Cyclic lambda calculi, Proc. of 3rd Int. Symp. on Theoretical Aspects of Computer Software, pp.77-106, 1997.
DOI : 10.1007/BFb0014548

Z. Ariola and M. Felleisen, The call-by-need lambda calculus, Journal of Functional Programming, vol.7, issue.3, pp.265-301, 1997.
DOI : 10.1017/S0956796897002724

Z. Ariola and J. Klop, Cyclic lambda graph rewriting, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.416-425, 1994.
DOI : 10.1109/LICS.1994.316066
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.7687

M. Flatt and P. , Reference: PLT Scheme, 2010.

J. Launchbury, A natural semantics for lazy evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.144-154, 1993.
DOI : 10.1145/158511.158618

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system, release 3, 2008.

E. Moggi and A. Sabry, An abstract monadic semantics for value recursion, RAIRO - Theoretical Informatics and Applications, vol.38, issue.4, pp.375-400, 2004.
DOI : 10.1051/ita:2004018

K. Nakata and M. Hasegawa, Small-step and big-step semantics for call-by-need, Journal of Functional Programming, vol.19, issue.06, pp.699-722, 2009.
DOI : 10.1007/BF01019945

M. Schmidt-schauß, D. Sabel, and E. Machkasova, Simulation in the call-by-need lambda-calculus with letrec, Proc. of 21st Int. Conf. on Rewriting Techniques and Applications Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.295-310, 2010.

P. Sestoft, Deriving a lazy abstract machine, Journal of Functional Programming, vol.7, issue.3, pp.231-264, 1997.
DOI : 10.1017/S0956796897002712

M. Sperber, K. Dybvig, M. Flatt, A. Straaten, R. Findler et al., Revised6 Report on the Algorithmic Language Scheme, Journal of Functional Programming, vol.4, issue.S1, pp.1-301, 2009.
DOI : 10.1023/A:1010051815785

D. Syme, Initializing Mutually Referential Abstract Objects: The Value Recursion Challenge, Proc. of the ACM-SIGPLAN Workshop on ML (ML 2005), pp.3-25, 2006.
DOI : 10.1016/j.entcs.2005.11.038

D. Syme, The F# programming language, version 2, 2010.

]. C. Allauzen and B. Durand, Appendix A: Tiling Problems The Classical Decision Problems, 1996.

R. Berger, The undecidability of the domino problem, Memoirs of the American Mathematical Society, vol.0, issue.66, 1966.
DOI : 10.1090/memo/0066

K. Culik, An Aperiodic Set of 13 Wang Tiles, Discrete Math, pp.245-251, 1996.

B. Durand, L. Levin, A. Shen, and C. Tilings, Abstract, See also Proc. 33rd Ann. ACM Symp. Theory Computing, pp.593-613, 2001.
DOI : 10.1016/0022-0000(91)90007-R
URL : https://hal.archives-ouvertes.fr/hal-00079709

B. Durand, A. Romashchenko, and A. Shen, Fixed-point tile sets and their applications, Journal of Computer and System Sciences, vol.78, issue.3
DOI : 10.1016/j.jcss.2011.11.001
URL : https://hal.archives-ouvertes.fr/lirmm-00736079

B. Durand, A. Romashchenko, and A. Shen, Effective Closed Subshifts in 1D Can Be Implemented in 2D
DOI : 10.1002/j.1538-7305.1961.tb03975.x

P. Gács, Reliable cellular automata with self-organization, Proceedings 38th Annual Symposium on Foundations of Computer Science, pp.45-267, 2001.
DOI : 10.1109/SFCS.1997.646097

J. Kari, A Small Aperiodic Set of Wang tiles, Discrete Math, pp.259-264, 1996.

J. Neumann, Theory of Self-reproducing Automata, 1966.

R. Robinson, Undecidability and nonperiodicity for tilings of the plane, Inventiones Mathematicae, vol.40, issue.3, pp.177-209, 1971.
DOI : 10.1007/BF01418780

C. Radin, Miles of tiles. Student Mathematical Library, 1994.

]. S. Bloom and Z. Esik, Iteration theories, EATCS Monographs on Theor. Comput. Sci, issue.1, 1993.
DOI : 10.1007/978-3-642-78034-9

E. Dubuc and R. Street, Dinatural transformations Reports of the Midwest Category Seminar IV, v. 137 of Lect, Notes in Math, pp.126-137, 1970.

P. Freyd, Algebraically complete categories, Proc. of, 1990.
DOI : 10.1007/BFb0084215

. Int and . Conf, on Category Theory (Como, pp.95-104, 1990.

P. Freyd, Remarks on algebraically compact categories, Applications of Categories in Computer Science, v. 177 of LMS Lect. Note Series, pp.95-106, 1992.
DOI : 10.1017/CBO9780511525902.006

N. Ghani, T. Uustalu, and V. Vene, Build, Augment and Destroy, Universally, Proc. of 2nd Asian Symp. on Programming Languages and Systems 3302 of Lect. Notes in Comput. Sci, pp.327-347, 2004.
DOI : 10.1007/978-3-540-30477-7_22
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.73.7890

M. Hasegawa, The uniformity principle on traced monoidal categories, Publications of the Research Institute for Mathematical Sciences, vol.40, issue.3, pp.991-10143, 2004.
DOI : 10.2977/prims/1145475500

P. S. Mulry, Strong monads, algebras and fixed points, Applications of Categories in Computer Science, v. 177 of LMS Lect. Note Series, pp.202-216, 1992.
DOI : 10.1017/CBO9780511525902.012

R. Paré and L. Roman, Dinatural numbers, Journal of Pure and Applied Algebra, vol.128, issue.1, pp.33-92, 1998.
DOI : 10.1016/S0022-4049(97)00036-4

D. Pavlovic, Logic of build fusion, 2000.

A. Simpson and G. Plotkin, Complete axioms for categorical fixed-point operators, Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pp.30-41, 2000.
DOI : 10.1109/LICS.2000.855753

T. Uustalu and V. Vene, In Abstracts of 12th Nordic Wksh. on Programming Theory Coding recursionàrecursion`recursionà la Mendler (extended abstract), ), 2 pp. Univ. i Bergen Proc. of 2nd Wksh. on Generic Programming Tech. rep. UU-CS, pp.69-85, 2000.

T. Uustalu and V. Vene, An alternative characterization of complete iterativeness (extended abstract), Proc. of 5th Int, pp.81-83, 2003.

T. Uustalu and V. Vene, The Recursion Scheme from the Cofree Recursive Comonad, Proc. of 2nd Wksh. on Mathematically Structured Functional Programming, 2008.
DOI : 10.1016/j.entcs.2011.02.020

. Proof, X. Let, A. , and T. Contractive, Then for any x 0 ? X, (T n x 0 ) n?N is a forward Cauchy sequence. Hence by Lemma 3.3, there exists ? ? AX that is fixed under T * . Now Theorem 3.1 applies and we get a fixed point of T . Since T is a contraction

. Knaster-tarski-'s-fixed, . Point, and J. Now, It is well-known that that any (·)-complete X is a complete lattice in the intrinsic order, and hence (·) is admissible. It is actually a metric version of Knaster-Tarski's theorem that we are going to prove

. Pattern-for-caristi-'s and . Bourbaki-witt, s fixed point theorems It is known from [6] that any complete metric space X can be embedded onto the set of maximal elements of a continuous dcpo BX := {{x, r | x ? X, ? > r 0} ? X, where x, r(z) := X(z, x) + r, and x, r BX y, s iff x, r X y, s iff r X(x, y) + s. In [9] it has been shown that X is an A-complete gms iff (BX, BX ) is a dcpo We will use this knowledge in proving a generalized version of Caristi's fixed point theorem

. Proof, Let Z be a subgms of BX consisting of elements of the form x, ?(x) for x ? X. Hence x, ?(x) Z y, ?(y) iff ?(x) X(x, y) + ?(y) Moreover ? is lower semicontinuous iff it preserves directed suprema with respect to the order Z . All this means that

A. Bauer, On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos, Electronic Notes in Theoretical Computer Science, vol.249, pp.157-167, 2009.
DOI : 10.1016/j.entcs.2009.07.089

M. Bonsangue, F. Van-breugel, and J. Rutten, Generalized metric spaces: Completion, topology, and powerdomains via the Yoneda embedding, Theoretical Computer Science, vol.193, issue.1-2, pp.1-51, 1998.
DOI : 10.1016/S0304-3975(97)00042-X

J. Caristi, Fixed point theorems for mapping satisfying inwardness conditions, Transactions of the, pp.241-251, 1976.

F. Dacar, Suprema of families of closure operators, Seminar for foundations of mathematics and theoretical computer science, Faculty of Mathematics and Physics Available on-line at: http://dis.ijs, 2008.

J. Dugundji and A. Granas, Fixed point theory, of Monografie Matematyczne, 1982.

A. Edalat and R. Heckmann, A computational model for metric spaces, Theoretical Computer Science, vol.193, issue.1-2, pp.53-73, 1998.
DOI : 10.1016/S0304-3975(96)00243-5

K. Goebel and W. A. Kirk, Topics in metric fixed point theory, of Cambridge Studies in Advanced Mathematics, 1990.
DOI : 10.1017/CBO9780511526152

M. Kostanek and P. Waszkiewicz, The formal ball model for -categories, Mathematical Structures in Computer Science, vol.17, issue.01
DOI : 10.1023/B:APCS.0000018144.87456.10

F. W. Lawvere, Metric spaces, generalized logic, and closed categories, Rendiconti del Seminario Matematico e Fisico di Milano, vol.43, issue.1, pp.135-1661, 1973.
DOI : 10.1007/BF02924844

D. Pataraia, A constructive proof of Tarski's fixed-point theorem for dcpos. 65th Peripatetic Seminar on Sheaves and Logic, 1997.

P. Waszkiewicz, On domain theory over Girard quantales, Fundamenta Informaticae, vol.92, pp.1-24, 2009.