Abstract
For programming languages whose denotational semantics uses fixed points of domain constructors of mixed variance, proofs of correspondence between operational and denotational semantics (or between two different denotational semantics) often depend upon the existence of relations specified as the fixed point of non-monotonic operators. This paper describes a new approach to constructing such relations which avoids having to delve into the detailed construction of the recursively defined domains themselves. The method is introduced by example, by considering the proof of computational adequacy of a denotational semantics for expression evaluation in a simple, untyped functional programming language.
Research supported by UK SERC grant GR/G53279, CEC ESPRIT project CLICS-II and CEC SCIENCE project PL910296
Preview
Unable to display preview. Download preview PDF.
References
P. J. Freyd. Recursive Types Reduced to Inductive Types. In Proc. 5th Annual Symp. on Logic in Computer Science, Philadelphia, 1990 (IEEE Computer Society Press, Washington, 1990), pp 498–508.
P. J. Freyd. Algebraically Complete Categories. In A. Carboni et al (eds), Proc. 1990 Como Category Theory Conference, Lecture Notes in Math. Vol. 1488 (Springer-Verlag, Berlin, 1991), pp 95–104.
P. J. Freyd. Remarks on algebraically compact categories. In M. P. Fourman, P. T. Johnstone and A. M. Pitts (eds), Applications of Categories in Computer Science, L.M.S. Lecture Note Series 177 (Cambridge University Press, 1992), pp 95–106.
C. A. Gunter. Semantics of Programming Languages. Structures and Techniques. (MIT Press, 1992.)
A. R. Meyer. Semantical Paradigms: Notes for an Invited Lecture. In Proc. 3rd Annual Symp. on Logic in Computer Science, Edinburgh, 1988 (IEEE Computer Society Press, Washington, 1988), pp 236–255.
R. E. Milne. The formal semantics of computer languages and their implementations, Ph.D. Thesis, Univ. Cambridge, 1973.
P. W. O'Hearn and R. D. Tennent. Relational Parametricity and Local Variables. In Conf. Record 20th Symp. on Principles of Programming Languages, Charleston, 1993 (ACM, New York, 1993), pp 171–184.
A. M. Pitts. A Co-induction Principle for Recursively Defined Domains, Theoretical Computer Science, to appear. (Available as Univ. Cambridge Computer Laboratory Tech. Rept. No. 252, April 1992.)
A. M. Pitts. Relational Properties of Recursively Defined Domains. In: Proc. 8th Annual Symp. on Logic in Computer Science, Montréal, 1993 (IEEE Computer Soc. Press, Washington, 1993), pp 86–97.
G. D. Plotkin. LCF Considered as a Programming Language, Theoretical Computer Science 5(1977) 223–255.
G. D. Plotkin. Lectures on Predomains and Partial Functions. Notes for a course at CSLI, Stanford University, 1985.
J. C. Reynolds. On the Relation between Direct and Continuation Semantics. In J. Loeckx (ed.), 2nd Int. Colloq. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 14 (Springer-Verlag, Berlin, 1974), pp 141–156.
D. S. Scott. Domains for Denotational Semantics. In M. Nielsen and E. M. Schmidt (eds), Proc. 9th Int. Coll. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 140 (Springer, Berlin, 1982), pp 577–613.
M. B. Smyth and G. D. Plotkin. The Category-Theoretic Solution of Recursive Domain Equations, SIAM J. Computing 11(1982) 761–783.
G. Winskel. The Formal Semantics of Programming Languages. An Introduction. (MIT Press, 1993.)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pitts, A.M. (1994). Computational adequacy via ‘mixed’ inductive definitions. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1993. Lecture Notes in Computer Science, vol 802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58027-1_3
Download citation
DOI: https://doi.org/10.1007/3-540-58027-1_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58027-0
Online ISBN: 978-3-540-48419-6
eBook Packages: Springer Book Archive