×

Full abstractness for a functional/concurrent language with higher-order value-passing. (English) Zbl 0912.68114

Summary: We study a language which combines sequential and concurrent control features. The functional fragment of the language resembles a call-by-value, nondeterministic version of PCF, as in [K. Siebert, Lect. Notes Comput. Sci. 664, 376-390 (1993; Zbl 0788.68092)]. This has been augmented with a new type for processes with constructors for the prefixing, choice and concurrency primitives of value-passing CCS. The main achievement of the paper is to provide a fully-abstract denotational model, specified using a domain equation, for the standard Morris-style testing preorder of \(\lambda\)-calculus terms, extended to this new setting. This was accomplished by casting our model in a logical form and providing the relevant completeness and definability results. In the course of the full abstraction argument we provided a proof system for satisfiability and proved it complete in the operational semantics (using the definability result). This system is of interest on its own and independent of the full abstraction result as it can be used to compute properties of complex program terms from such of simple terms. The logical language we have introduced can be thought of as specifying a type system for the programming language. We have kept this system simple, introducing logical operators (type constructors) only to the extent necessary for our main results. However it would be interesting to make the type system more expressive, for example by adding a fixpoint operator, and in this way obtain a language for expressing nontrivial behavioral properties of processes and an associated proof system.

MSC:

68Q45 Formal languages and automata

Citations:

Zbl 0788.68092

Software:

Facile
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S., A domain equation for bisimulation, Inform. and Comput., 92, 161-218 (1991) · Zbl 0718.68057
[2] Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science (1994), Clarendon PressOxford Science Publications: Clarendon PressOxford Science Publications Oxford · Zbl 0829.68111
[3] Abramsky, S., Domain theory in logical form, Ann. Pure Appl. Logic, 51, 1-77 (1991) · Zbl 0737.03006
[4] Amadio, R. M., Technical Report (1994)
[5] Barendregt, H. P., The \(λ (1984)\), North-Holland: North-Holland Amsterdam · Zbl 0551.03007
[6] Boudol, G., A \(λ\), Inform. Comput., 108, 51-127 (1994) · Zbl 0796.03021
[7] Barendregt, H.; Coppo, M.; Dezani-Ciancaglini, M., A filter model and the completeness of type assignment, J. Symbolic Logic, 48, 931-940 (1983) · Zbl 0545.03004
[8] Damiani, F. Dezani-Ciancaglini, M. Giannini, P. A filter model for mobile processes, Math. Str. Comp. Sci.; Damiani, F. Dezani-Ciancaglini, M. Giannini, P. A filter model for mobile processes, Math. Str. Comp. Sci. · Zbl 0923.68088
[9] Dezani-Ciancaglini, M.; de’Liguoro, U.; Piperno, A., Filter models for a parallel and non deterministic \(λ\), Proc. Mathematical Foundations of Computer Science 1993. Proc. Mathematical Foundations of Computer Science 1993, LNCS 711 (1993), Springer-Verlag: Springer-Verlag Berlin, p. 403-412
[10] Giacalone, A.; Mishra, P.; Prasad, S., FACILE: A symmetric integration of concurrent and functional programming, Int. J. Parallel Program., 15, 121-160 (1989)
[11] Ferreira, W.; Hennessy, M.; Jeffrey, A., A theory of weak bisimulation for core CML, Proceedings of ACM SIGPLAN Int. Conf. Functional Programming. Proceedings of ACM SIGPLAN Int. Conf. Functional Programming, LNCS (1996), Assoc. Comput. Mach: Assoc. Comput. Mach New York, p. 201-212 · Zbl 1345.68049
[12] Ferreira, W.; Hennessy, M., Towards a semantic theory for CML, (Wiedermann, J.; Hájek, P., Proc. Mathematical Foundations of Computer Science 1995. Proc. Mathematical Foundations of Computer Science 1995, LNCS 969 (1995), Springer-Verlag: Springer-Verlag Berlin), 454-466 · Zbl 1193.68068
[13] Fereira, W.; Hennessy, M.; Jeffrey, A., Report (1996)
[14] Fournet, C.; Gonthier, G., The reflexive CHAM and the join-calculus, Proc. 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proc. 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Assoc. Comput. Mach. (1994), p. 372-385
[15] Jeffrey, A., A fully abstract semantics for a concurrent functional language with monadic types, Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science. Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1995), p. 244-254
[16] Hartonas, C., Duality for modal \(μ\), Theoretical Comput. Sci. (1998) · Zbl 0909.03021
[17] Hartonas, C.; Hennessy, M., Full abstraction for a functional/concurrent language with higher-order value-passing (extended abstract), Proc. Computer Science Logic, CSL 97. Proc. Computer Science Logic, CSL 97, LNCS 1414 (1998), Springer-Verlag: Springer-Verlag Berlin, p. 239-354
[18] Hennessy, M., An Algebraic Theory of Processes (1988), MIT Press: MIT Press Cambridge
[19] Hennessy, M., A fully abstract denotational model for higher-order processes, Inform. and Comput., 112, 55-95 (1994) · Zbl 0806.68071
[20] Hennessy, M. Higher-order processes and their models, Proceedings, 21st International Colloquium on Automata, Languages and Programming, S. AbiteboulE. Shamir, LNCS 820, 286, 303, Springer-Verlag, Berlin; Hennessy, M. Higher-order processes and their models, Proceedings, 21st International Colloquium on Automata, Languages and Programming, S. AbiteboulE. Shamir, LNCS 820, 286, 303, Springer-Verlag, Berlin · Zbl 0806.68071
[21] Larsen, K. G., Proof systems for satisfiability in Hennessy-Milner logic with recursion, Theoret. Comput. Sci., 72, 265-288 (1990) · Zbl 0698.68014
[22] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs · Zbl 0683.68008
[23] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes I, II, Inform. and Comput., 100, 1-40 (1992) · Zbl 0752.68036
[24] Moggi, E., Notions of computation and monads, Inform. and Comput., 93, 55-92 (1991) · Zbl 0723.68073
[25] Morris, J., Lambda-Calculus Models of Programming Languages (1968), MITPh.D. thesis
[26] Plotkin, G., A powerdomain construction, SIAM J. Comput., 5, 452-487 (1976) · Zbl 0355.68015
[27] Plotkin, G., LCF considered as a programming language, Theoret. Comput. Sci., 5, 323-355 (1997)
[28] Reppy, J. H., A higher-order concurrent language, Proceedings of the ACM SIGPLAN ‘91 PLDI, SIGPLAN Notices (1991), Assoc. Comput. Mach: Assoc. Comput. Mach New York, p. 294-305
[29] Reppy, J. H., Higher-Order Concurrency (1991), Cornell UniversityPh.D. thesis
[30] Reppy, J., CML: A higher-order concurrent language, Proc. ACM-SIGPLAN ‘91, Conf. on Programming Language Design and Implementation (1991), Assoc. Comput. Mach: Assoc. Comput. Mach New York
[31] Sangiorgi, D. Bisimulation in higher-order calculu, Inform. and Comput.; Sangiorgi, D. Bisimulation in higher-order calculu, Inform. and Comput. · Zbl 0876.68042
[32] Sieber, K., Call-by-value and nondeterminism, (Bezen, M.; Groote, J. F., Typed \(λ\). Typed \(λ\), LNCS 664 (1993), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0788.68092
[33] Stark, I., A fully-abstract domain model for the \(π\), Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science. Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1996), p. 36-42
[34] Stirling, C., A proof-theoretic characterization of observational equivalence, Theoret. Comput. Sci., 39, 27-45 (1985) · Zbl 0567.68020
[35] Stirling, C., Modal logics for communicating systems, Theoret. Comput. Sci., 49, 311-347 (1987) · Zbl 0624.68019
[36] Thomsen, B., Calculi for Higher-Order Communicating Systems (1990), Imperial CollegePh.D. thesis
[37] Thomsen, B., Plain chocs: A second generation calculus for higher order processes, Acta Informatica, 30, 1-59 (1993) · Zbl 0790.68069
[38] Winskel, G., A complete proof system for SCCS with modal assertions, (Maheshwari, S., Proceedings, 5th Conference on Foundations of Software Technology and Theoretical Computer Science. Proceedings, 5th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 206 (1985), Springer-Verlag: Springer-Verlag Berlin), 392-410 · Zbl 0586.68024
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.