Abstract
We have applied various results about the synthetic approach to domain theory to describe a PER-like model of the language Quest. Besides, we have presented a different model for Quest which allows the interpretation of the recursive operator at all types. This seems to be the first such in the literature, and we are certain that it could be given thanks to the tools provided by categorical logic. It also seems possible to relate the first model we have given with that of good PER's of Abadi and Plotkin, and that the two are essentially different. But we believe that the good PER's may provide a new interpretation for Quest in the spirit of our second model.
Another direction for development is to take the category of replete objects in a model for Synthetic Domain Theory as presented by Hyland in [10]. Such a model should give a smaller, more suitable collection of types than any of those given here.
We suspect that the nature of the second model is similar to those suggested in [3], but at the moment we know too little about that paper to comment further.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and G. Plotkin. A per model of polymorphism and recursive types. In Mitchell [16], pages 355–365.
R. Amadio. Recursion over realizability structures. Inform. and Comput., 91:55–85, 1991.
V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance and explicit coercion. In Meyer [15],, pages 112–129.
L. Cardelli and G. Longo. A semantic basis for Quest. SRC Research Report 55, Digital Equipment Corporation, 1989.
T. Coquand. Categories of embeddings. Theoretical Comput. Sci., 68:221–237, 1989.
P. Freyd. Recursive types reduced to inductive types. In Mitchell [16],, pages 498–507.
P. Freyd, P. Mulry, G. Rosolini, and D. Scott. Extensional PERs. In Mitchell [16],, pages 346–354.
P. Freyd, E. Robinson and G. Rosolini. Functorial parametricity. Report 12/91, Univ. of Sussex, 1991.
J. Hyland. The effective topos. In A. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165–216. North Holland Publishing Company, 1982.
J. Hyland. First steps in Synthetic Domain Theory. In A. Carboni, M. Pedicchio, and G. Rosolini. editors, Category Theory '90, Lectures Notes in Mathematics vol. 1488, pages 131–156, Como, July 1990. Springer-Verlag, 1991.
J. Hyland, P. Johnstone, and A. Pitts. Tripos Theory. Math. Proc. Camb. Phil. Soc., 88:205–232. 1980.
J. Hyland and A. Pitts. The theory of constructions: categorical semantics and topostheoretic models. In J. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, Contemp. Math. vol. 92, pages 137–199, Boulder, June 1987. A.M.S., 1989.
J. Hyland, E. Robinson, and G. Rosolini. The discrete objects in the effective topos. Proc. London Math. Soc, 60:1–60, 1990.
S. Maclane. Categories for the Working Mathematician. Springer-Verlag, 1971.
A. Meyer, editor. Logic in Computer Science, 4th Symposium, Asilomar. I.E.E.E. Computer Society, 1989.
J. Mitchell, editor. Logic in Computer Science, 5th Symposium, Philadelphia. I.E.E.E. Computer Society, 1990.
W. Phoa. Effective domains and intrinsic structure. In Mitchell [16],, pages 366–377.
W. Phoa. Two results on set-theoretic polymorphism. In D. Pitt, A. Pitts, A. Poigné, and D. Rydeheard, editors. Category theory and Computer Science, Lectures Notes in Computer Science vol. 530, Paris. Springer-Verlag, 1991. To appear.
E. Robinson. How complete is PER? In Meyer [15], pages 106–111.
G. Rosolini. Categories and effective computations. In D. Pitt, A. Poigné, and D. Rydeheard, editors, Category theory and Computer Science, Lectures Notes in Computer Science vol. 283, pages 1–11, Edinburgh. Springer-Verlag, 1987.
G. Rosolini. About modest sets. Int. J. Found. Comp. Sci., 1:341–353, 1990.
D. Scott. Church's thesis and a unification of types. Lecture at the Conference on Church's Thesis: fifty years later.
R. Seely. Categorical models for higher order polymorphic typed lambda calculus. Journ. Symb. Logic, 52:969–989, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rosolini, G. (1992). An exper model for Quest. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1991. Lecture Notes in Computer Science, vol 598. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55511-0_22
Download citation
DOI: https://doi.org/10.1007/3-540-55511-0_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55511-7
Online ISBN: 978-3-540-47194-3
eBook Packages: Springer Book Archive