Abstract
Following Scott, the denotational semantics of programming languages are usually built from the notion of continuous functions. The need for restricted models has been emphasized by Plotkin and Milner, which showed thats continuous function models did not capture all operational properties of ALGOL-like sequential languages. We present new model constructions from a notion of stable function. This requires the introduction of two different orderings between stable functions which give very different cpo structures to the function spaces. We show that Milner's fully abstract model of Plotkin's PCP language only contains stable functions.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
Bibliography
G. BERRY, "Bottom-up Computations of Recursive Programs", R.A.I.R.O. Informatique Theorique, vol.10, no 3, mars 1976, pp 47–82.
G. BERRY, "Séquentialité de l'Evaluation formelle des λ-expressions", Proc. 3rd International Colloquium on Programming, Paris, march 28–30, 1978, DUNOD.
G. BERRY, "Calculs Optimaux des Programmes dans les Interprétations stables", Thèse de doctorat d'Etat, to appear.
G. BERRY, P.L. CURIEN, "Sequential Computations in Concrete Data structures", to appear.
G. BERRY, J.J. LEVY, "Minimal and Optimal Computations of Recursive Programs", Proc. 3rd ACM Symposium on Principles of Programming Languages, Los Angeles, jan. 1977. To appear in JACM.
B. COURCELLE, J.C. RAOULT, "Completion of ordered magmas", Fondamenta Informatica, Poland 1978, to appear.
G. KAHN, G. PLOTKIN, "Concrete Data Structures", to appear.
J.J. LEVY, "An algebraic interpretation of the λβκ-calculus and an application of a labelled λ-calculus", Rome, 1975 and TCS, vol. 2, no 1, 1976, p. 97–114.
J.J. LEVY, "Réductions correctes et optimales dans le λ-calcul", Thèse de doctorat d'Etat, Univ. Paris VII, jan. 1978.
R. MILNER, "Implementation and application of Scott's logic for computable functions", Proc. ACM Conference on Proving Assertions about Programs, SIGPLAN Notices 7, 1 (jan. 1972) 1–6.
R. MILNER, "Models of LCF", Stanford Comp. Sci. Dept. Memo. CS-73-332, Stanford, 1973.
R. MILNER, "Fully Abstract Models of typed λ-calculi", T.C.S. vol. 4, no 1, feb. 1977, pp. 1–23.
G.D. PLOTKIN, "LCF as a Programming Language", Proc. Conf. Proving and Improving Programs, Arc-et-Senans, France, 1975, and T.C.S. vol. 5, no 3, 1977, pp. 223–257.
G.D. PLOTKIN, "A Powerdomain Construction", SIAM Journal of Computing, Vol. 5, no 3, sept. 1976.
G.D. PLOTKIN, M. SMYTH, "The category-theoretic solution of recursive domain equations", Proc. 18 th Annual Symposium on Foundations of Computer Science, Oct. 31 — Nov. 2, 1977.
V. Yu. SAZONOV, "Sequentially and Parallelly Computable functionals", Rome, march 75. Springer — Verlag LNCS no 37.
D. SCOTT, "Data types as Lattices", Lecture Notes, unpublished, Amsterdam 1972.
D. SCOTT, "Outline of a mathematical theory of Computation", Proc. 4th Ann. Princeton Conf. on Information Sciences and Systems, Princeton Univ., Princeton, N.J., 1970, pp 169–176.
J. VUILLEMIN, "Proof Techniques for Recursive Programs", Ph. D. Thesis, Stanford University, 1973.
C.P. WADSWORTH, "The relation between Operational and Denotational properties for Scott's D∞ model of the λ-calculus, SIAM Journal of Computing, vol. 5, no 3, sept. 1976.
M. WAND, "Fixed — Points Constructions in order-enriched Categories", TR 23, Comp. Sci. Dept. Indiana Univ., 1975.
P.H. WELCH, "Continuous Semantics and Inside-out Reductions", Rome, 1975, Springer Verlag, LNCS no 37.
G. HUET, "Résolution d'équations dans les langages d'ordre 1,2,...,ω". Thèse d'Etat, Université PARIS VII, Paris, Sept. 1976.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1978 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berry, G. (1978). Stable models of typed λ-calculi. In: Ausiello, G., Böhm, C. (eds) Automata, Languages and Programming. ICALP 1978. Lecture Notes in Computer Science, vol 62. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-08860-1_7
Download citation
DOI: https://doi.org/10.1007/3-540-08860-1_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-08860-8
Online ISBN: 978-3-540-35807-7
eBook Packages: Springer Book Archive