Abstract
We study the longstanding problem of semantics for input/output (I/O) expressed using side-effects. Our vehicle is a small higher-order imperative language, with operations for interactive character I/O and based on ML syntax. Unlike previous theories, we present both operational and denotational semantics for I/O effects. We use a novel labelled transition system that uniformly expresses both applicative and imperative computation. We make a standard definition of bisimilarity and prove it is a congruence using Howe's method.
Next, we define a metalogical type theory M in which we may give a denotational semantics to O.M generalises Crole and Pitts' FIX-logic by adding in a parameterised recursive datatype, which is used to model I/O. M comes equipped both with judgements of equality of expressions, and an operational semantics; M itself is given a domain-theoretic semantics in the category CPPO of cppos (bottom-pointed posets with joins of ω-chains) and Scott continuous functions. We use the CPPO semantics to prove that the equational theory is computationally adequate for the operational semantics using formal approximation relations. The existence of such relations uses key ideas from Pitts' recent work.
A monadic-style textual translation into M induces a denotational semantics on O. Our final result justifies metalogical reasoning: if the denotations of two O programs are equal in M then the O programs are in fact operationally equivalent.
Preview
Unable to display preview. Download preview PDF.
References
Samson Abramsky and Luke Ong. Full abstraction in the lazy lambda calculus. Information and Computation 105:159–267, 1993.
Dave Berry, Robin Milner, and David N. Turner. A semantics for ML concurrency primitives. In 19th POPL, pages 119–129, 1992.
Gérard Boudol. Towards a lambda-calculus for concurrent and communicating systems. In TAPSOFT'89, Springer LNCS 351, 1989.
Roy. L. Crole. Categories for Types. CUP, 1993.
Roy. L. Crole and A. M. Pitts. New foundations for fixpoint computations: FIX hyperdoctrines and the FIX-logic. Information and Computation, 98:171–210, 1992.
Roy L. Crole. Programming Metalogics with a Fixpoint Type. PhD thesis, University of Cambridge, 1992.
Roy L. Crole and Andrew D. Gordon. Factoring an adequacy proof (preliminary report). In Functional Programming, Glasgow 1993, Springer 1994.
Marcello P. Fiore and Gordon D. Plotkin. An Axiomatisation of Computationally Adequate Domain Theoretic Models of FPC. In 9th LICS, 1994.
P. Freyd. Algebraically complete categories. In 1990 Como Category Theory Conference, Springer Lecture Notes in Mathematics, 1991.
Andrew D. Gordon. Functional Programming and Input/Output. CUP, 1994.
Andrew D. Gordon. An operational semantics for I/O in a lazy functional language. In FPCA'93, pages 136–145. 1993.
Andrew D. Gordon. A tutorial on co-induction and functional programming. In Functional Programming, Glasgow 1994. Springer Workshops in Computing.
Sören Holmström. PFL: A functional language for parallel programming. Report 7, Chalmers PMG. 1983.
Douglas J. Howe. Equality in lazy computation systems. In 4th LICS, 1989.
John McCarthy et al. LISP 1.5 Programmer's Manual. MIT Press, 1962.
Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.
R. Milner, M. Tofte and R. Harper. The Definition of SML. MIT Press, 1990.
Peter D. Mosses. Denotational semantics. In Jan Van Leeuven, editor, Handbook of Theoretical Computer Science, pages 575–631. Elsevier 1990.
Eugenio Moggi. Notions of computations and monads. TCS, 93:55–92, 1989.
Andrew M. Pitts. Evaluation logic. In IVth Higher Order Workshop, Banff 1990, pages 162–189. Springer 1991.
Andrew M. Pitts. Relational properties of domains. Tech. Report 321, University of Cambridge Computer Laboratory, December 1993.
Andrew M. Pitts. Computational adequacy via ‘mixed’ inductive definitions. In MFPS IX, New Orleans 1993, pages 72–82, Springer LNCS 802, 1994.
Gordon D. Plotkin. Pisa notes on domains, June 1978.
Gordon D. Plotkin. Denotational semantics with partial functions. Stanford CSLI 1985.
Jonathan Rees and William Clinger. Revised3 report on the algorithmic language scheme. ACM SIGPLAN Notices, 21(12):37–79, December 1986.
Philip Wadler. The essence of functional programming. In 19th POPL, 1992.
John H. Williams and Edward L. Wimmers. Sacrificing simplicity for convenience: Where do you draw the line? In 15th POPL, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Crole, R.L., Gordon, A.D. (1995). A sound metalogical semantics for input/output effects. In: Pacholski, L., Tiuryn, J. (eds) Computer Science Logic. CSL 1994. Lecture Notes in Computer Science, vol 933. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022267
Download citation
DOI: https://doi.org/10.1007/BFb0022267
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60017-6
Online ISBN: 978-3-540-49404-1
eBook Packages: Springer Book Archive