Mathematical foundations of programming semantics. 5th international conference, New Orleans, Louisiana, USA, March 29 -- April 1, 1989. Proceedings (Q1188840)

The articles of this volume will be reviewed individually. For the 1987 workshop see [Zbl 0635.00016]. This proceedings report on the 5th international conference on the Mathematical Foundations of Programming Semantics held in 1989 at Tulane University, New Orleans, Louisiana. The major goal of the conference was to bring computer scientist working in programming semantics and mathematicians who work in areas which might impact programming semantics together for sharing ideas and discussing problems of mutual interest. \textit{S. Abramsky} contributes a preliminary investigation on a generalized version of the Kahn principle valid for a large class of abstract asynchronous networks. \textit{L. Cardelli} and \textit{J. C. Mitchell} discuss a second order type system with subtyping and polymorphism over operations for creating and manipulating records. \textit{E. W. Stark} studies concurrent transition systems: For trace automata over a concurrency alphabet the notion of a residual of one computation `after' another induces a preorder which is equivalent to the permutation preorder. Reformulation of the properties of the residual operation yields a category of concurrent transition systems. This category provides a framework for showing the relationship between domains of permutation equivalence classes generated by a trace automaton and the normal subdomains of the domain of traces over the concurrency alphabet. \textit{G. M. Reed} presents a hierarchy of models for real-time versions of CSP which support timewise refinement and the development of proof systems. \textit{J. Davies} and \textit{S. Schneider} contribute, based on the above mentioned work of Reed, a simple notion of behavioral specifications for Timed CSP together with a complete set of inference rules. \textit{A. W. Roscoe} and \textit{G. Barrett} extend the failure/divergence model for CSP: By adding a component for infinite behaviors a denotational semantics including arbitrary nondeterminism and infinite hiding can be defined. Since the employed semantical domain is incomplete, special attention is paid to deal with fixed point constructions. Finally, the denotational model is shown to be equivalent to an operational one. \textit{G. Barrett} presents an operational semantics for occam treating priority as well as fairness. \textit{F. Pfenning} and \textit{C. Paulin-Mohring} introduce the notion of inductively defined type in the calculus of constructions and discuss the representation and induction for this kind of types. \textit{K. Malmkjær} provides a framework for a denotational semantics for a reflective tower. The framework is used to analyze a reflective tower for scheme. \textit{M. G. Main} and \textit{D. L. Black} show the use of assertional \(s\)- rings for algebraic description of fair infinite behaviors and reasoning about termination under fairness conditions for non-deterministic iterative programs. \textit{A. Stoughton} shows the existence of equational fully abstract models that are not inequationally fully abstract. \textit{L. S. Moss} and \textit{S. R. Thatt} contribute a paper entitled ``Generalization of final algebra semantics by relativization''. \textit{L. Aceto} and \textit{M. Hennessy} provide operational and denotational interpretations for a process algebra with explicit representation of successful termination, deadlock and divergence. Starting from a set of inequations for processes, a denotational model is obtained as the initial continuous algebra induced by this set of inequations. An operational model is given by a transition system together with predicates for successful termination and divergence. It is argued that a behavioral preorder (with additional restrictions concerning finite approximation and context preservation) coincides with the order induced by the inequations on the denotational model. \textit{P. Panangaden} and \textit{J. R. Russell} present a category-theoretic semantics for a simple imperative language with unbounded indeterminacy in the form of random assignment. The denotational semantics is based on a categorical powerdomain of multi-sets over a flat cpo, adapted from Lehmann. The model is \(\omega\)-continuous in the treatment of while loops by means of colimits of \(\omega\)-diagrams. After application of a (non- continuous) abstraction function the categorial semantics yields a fully abstract model w.r.t. a natural operational one. \textit{J. M. E. Hyland}, \textit{E. P. Robinson} and \textit{G. Rosolini} study the construction of PER models for second order lambda calculus which are initial algebras. \textit{E. L. Gunter} proposes the notion of a local lattice that extends the notion of an \(L\)-domain as the category of domains for mathematical foundations of denotational semantics. \textit{R. Jagadeesan} has a submission entitled ``\(L\)-domains and lossless powerdomains''. \textit{A. Pasztor} shows that, in the framework of first order temporal logic, there exists an infinite hierarchy of verification methods between the some-other-time and the some-time methods. \textit{A. J. Power} uses enriched categories and monads to give an algebraic formulation for date refinement. \textit{He Jifeng} and \textit{C. A. R. Hoare} discuss the use of 2-categories for the definition of conventional programming language constructs. \textit{J. W. Gray} presents a paper `` Initial algebra semantics for lambda calculi''. Indexed articles: \textit{Abramsky, Samson}, A generalized Kahn principle for abstract asynchronous networks, 1-21 [Zbl 07673895] \textit{Cardelli, Luca; Mitchell, John C.}, Operations on records (summary), 22-52 [Zbl 07673896] \textit{Stark, Eugene W.}, Connections between a concrete and an abstract model of concurrent systems, 53-79 [Zbl 07673897] \textit{Reed, G. M.}, A hierarchy of domains for real-time distributed computing, 80-128 [Zbl 07673898] \textit{Davies, Jim; Schneider, Steve}, Factorizing proofs in timed CSP, 129-159 [Zbl 07673899] \textit{Roscoe, A. W.; Barrett, Geoff}, Unbounded nondeterminism in CSP, 160-193 [Zbl 07673900] \textit{Barrett, Geoff}, The semantics of priority and fairness in occam, 194-208 [Zbl 07673901] \textit{Pfenning, Frank; Paulin-Mohring, Christine}, Inductively defined types in the calculus of constructions, 209-228 [Zbl 07673902] \textit{Malmkjær, Karoline}, On some semantic issues in the reflective tower, 229-246 [Zbl 07673903] \textit{Main, Michael G.; Black, David L.}, Semantic models for total correctness and fairness, 247-270 [Zbl 07673904] \textit{Stoughton, Allen}, Equationally fully abstract models of PCF, 271-283 [Zbl 07673905] \textit{Moss, Lawrence S.; Thatte, Satish R.}, Generalization of final algebra semantics by relativization, 284-300 [Zbl 07673906] \textit{Aceto, L.; Hennessy, M.}, Termination, deadlock and divergence, 301-318 [Zbl 07673907] \textit{Panangaden, Prakash; Russell, James R.}, A category-theoretic semantics for unbounded indeterminacy, 319-332 [Zbl 07673908] \textit{Hyland, J. M. E.; Robinson, E. P.; Rosolini, G.}, Algebraic types in PER models, 333-350 [Zbl 07673909] \textit{Gunter, Elsa L.}, Pseudo-retract functors for local lattices and bifinte L-domains, 351-363 [Zbl 07673910] \textit{Jagadeesan, Radhakrishnan}, L-domains and lossless powerdomains, 364-372 [Zbl 07673911] \textit{Pasztor, Ana}, Does ``N+1 times'' prove more programs correct than ``N times''?, 373-389 [Zbl 07673912] \textit{Power, A. J.}, An algebraic formulation for data refinement, 390-401 [Zbl 07673913] \textit{Jifeng, He; Hoare, C. A. R.}, Categorical semantics for programming languages, 402-417 [Zbl 07673914] \textit{Gray, John W.}, Initial algebra semantics for lambda calculi, 418-439 [Zbl 07673915]