The construction of reliable software from specifications requires a large body both of theoretical results and of practical tools to be successful. Theoretical results run the gamut of several mathematical disciplines: category theory, domain theory, universal algebra and various areas of logic, to name a few. Several practical tools now are available, a number of which offer the possibility of checking programs against their specifications. As these theories and tools evolve and are further developed, it is important to make them known and available both to researchers and to practitioners. It also is important that workers in the many areas involved have opportunities to meet so they can exchange ideas, inform others of their latest results, and become acquainted with what others are doing that is related to their own work.

A series of meetings that has emphasized the range of theoretical topics just described is the Mathematical Foundations of Programming Semantics (MFPS). MFPS has met annually since 1985, alternating between a workshop format in which all participants are invited to give talks about their latest results, and a conference format in which papers are selected for presentation from submissions received in response to a Call for Papers.

In both cases, Proceedings volumes are published; in the case of workshops, these take the form of special issues of Theoretical Computer Science, while conference Proceedings take the form of volumes of LNCS, or, most recently, of the new electronic series Electronic Notes in Theoretical Computer Science (cf. http://www.elsevier.nl/locate/entcs). ENTCS is an excellent mechanism for disseminating the results of workshops and conferences, and as the founding editor of ENTCS, I would welcome proposals from the organizers of Brazilian meetings to publish their proceedings in the series.

Over the years, MFPS has come to be regarded among the top meetings for researchers interested in theoretical computer science and its mathematical underpinnings, comparable with such European series as ICALP and CONCUR. In fact, MFPS has attracted remarkable interest from the European community where the theory we have described has its roots. It has enjoyed regular participation by such renowned researchers as Samson Abramsky (Edinburgh), Robin Milner (Cambridge) and Gordon Plotkin (Edinburgh), as well as US researchers such as John Mitchell (Stanford). John Reynolds (Carnegie Mellon) and Dana Scott (Carnegie Mellon).

MFPS also has tried to include researchers in the more practical, implementation-oriented aspects of software development as participants. The list of people with this viewpoint who have been invited speakers includes Neil Jones (DIKU), Luca Cardelli (DEC SRC). Colin Stirling (Edinburgh), Gerard Berry (INRIA), Edmund Clarke (CMU), and Gerard Huet (INRIA). We also have featured software tools at our meetings, providing researchers with a chance to become acquainted with the latest methods for automating aspects of software development.

We believe that an effective method for stimulating interaction between the Brazilian research community and its US counterpart would be through participation by members of the former in the MFPS series. Given the existing ties between the Brazilian research and development communities and those in Europe, MFPS seems a logical venue to provide an entree into the US community. Participation in MFPS by Brazilian researchers could be accomplished by several means. First, the Brazilian National Science Foundation could help support some researchers to attend MFPS meetings. The next MFPS meeting will be held on the campus of Carnegie Mellon University in March, 1997. Information about the meeting, including the Program is available at the URL

The MFPS home page is http://www.math.tulane.edu/MFPS.html. A method for enhancing this participation would be to have information about MFPS sent to Brazilian researchers. As one of the organizers of the series (the others are Stephen Brookes (Carnegie Mellon), Michael Main (Colorado), Austin Melton (Kent State) and David Schmidt (Kansas State)), I would be happy to write a general letter of invitation that could be disseminated to the Brazilian research community, perhaps under the auspices of CNPq. By providing support for a limited number of Brazilians to attend MFPS - even if they do not present papers - CNPq would give Brazilian researchers an ideal opportunity to learn of the latest theoretical developments in the US community and a chance to get to know some of the leading US researchers.

While stimulating participation in MFPS clearly is a good method to engender interaction between Brazilian researchers and their US counterparts, such interaction will not occur without common interests. Toward that end, I briefly describe some of my own interests that I believe could be shared with researchers in Brazil.

Domain theory, the topic founded by Dana Scott (Carnegie Mellon University) in the 1960s when he discovered the first mathematical model of the untyped lambda calculus, forms the heart of my research interests. This theory has developed to a point that it now provides a firm, mathematical foundation for the most widely-accepted approach to building denotational (ie, mathematical) models for programming languages. Recently, its applications have expanded greatly through the work of Abbas Edalat (Imperial College). Edalat has found methods for applying domain theory to derive new approaches to such wide-ranging topics as fractals, neural networks, and real analysis.

My recent work has focused on questions of how to modularize the building of denotational and related operational models for programming languages. In joint work with Frank Oles (IBM), I have shown that the first-order languages such as are common in process algebra are amenable to such methods. In particular, Oles and I have shown that full abstraction can be lifted from the level of a language without identifiers to the sublanguage of closed terms in the extension of the original language that includes identifiers and recursion operators. This result applies in the setting of domain theory - both the denotational and operational models must be ordered structures, and the denotational model must be an algebraic domain in which all the compact elements are denotable. The extension applies to models that satisfy equations and inequalities, as well as those that are anomic.

Work on this question of modularizing the construction of fully abstract models has led me to consider some of the standard constructions of domain theory, such as the construction of power domains, and initial continuous algebras in general. These constructions - for algebraic domains - invariably involve a related construction at the level of the compact elements which then is lifted using the ideal completion to the level of domains. But this approach is not functorial - at least on the surface; since continuous maps in general do not preserve compact elements, the association of the set of compact elements to an algebraic domain does not extend to a functor. A result I announced at MFPS last spring shows that this approach indeed can be made functorial - ie, initial algebras can be constructed at the poset level on the set of compact elements, and then lifted to the domain level, so that the whole process is functorial. The result relies on a general category theory result, and exploits the fact that, for example, the category of algebraic domains and continuous maps is the Kleisli category for the monad that is generated by the ideal functor from posets and monotone maps to cpos and continuous maps, which is left adjoint to the inclusion.

This result also has led me to a better understanding of the recent work of Abramsky and Jung, who devised a new approach to continuous domains using the idea of abstract bases, first investigated by Michael Smyth. The result described in the previous paragraph can be applied to this setting, but it requires one to generalize the setting Abramsky and Jung devised. In their approach, morphisms between abstract bases are approximable relations, and this results in a category that is equivalent to that of continuous domains and continuous maps. To have a meaningful extension of the result I described for algebraic domains, one needs more general mappings. These are called the "ideal mappings" between abstract bases; they are so named because they are exactly the ones that induce continuous mappings between the respective ideal completions. Just as there are more monotone mappings between posets than continuous ones, there are more ideal mappings between abstract bases than there are approximable mappings. The result is that the construction of initial continuous algebras in the category of continuous domains and continuous mappings can be carried out first in the category of abstract bases and ideal mappings, and then lifted using the ideal completion functor so that the whole process is functorial. In fact, on the object level this is exactly how the construction is presented in Abramsky and Jung; the result described above shows that their construction actually is functorial and results in the initial algebra in the category of continuous domains without further ado.

In addition to domain theory and related topics, the area of concurrency is a focal point for my interests, and principally the language CSP. This language for reasoning about distributed systems was first devised by C. A. R. Hoare and members of his school at Oxford, most notably recently by A. W. Roscoe and G. M. Reed. Because of their regular participation in MFPS (indeed, MFPS was held at Oxford in 1992), I have developed an on-going collaboration with members of the Oxford group. My collaboration has focused on one particular aspect - unbounded nondeterminism.

Unbounded nondeterminism is useful - in some sense required - to have a theory adequate to model process refinement. In the setting of untimed and Timed CSP, where many models are available to provide a varying array of levels of abstraction at which to consider processes and their specifications, unbounded nondeterminism is necessary in moving from one level to another. Roscoe devised the first model for unbounded nondeterminism for CSP, together with his student Barrett, in the untimed setting. Steve Schneider, then a student of Reed, was led to consider this same topic in his attempts to devise refinement operators between the untimed and Timed worlds that CSP offers.

The results that I have been involved in here are ones of a theoretical nature again. Inspired by results about CSP and models for unbounded nondeterminism, Roscoe, Steve Schneider and I were led to consider more general structures than domains. These were needed since their results already showed that one was forced to consider incomplete structures and to move from continuous to monotone mappings in devising models for unbounded choice. Our joint work found a common theme to the approach they both had devised, a theme that resides in the realm of what we called local cpos - partial orders in which the lower set of each point is directed complete, but which are not necessarily directed complete as a whole. In order to prove the existence of least fixed points which are the basic substance of domain theoretic models, we had to devise a dominated convergence theorem. It states that, in a local cpo which is generated by a cpo, every monotone selfmap that is dominated by a monotone selfmap on the generating cpo must have a least fixed point. By embedding the model for bounded nondeterminism in the model for unbounded nondeterminism in such a way that the bounded nondeterminism model - which is a cpo - generates the local cpo that serves to model unbounded nondeterminism, we are in a setting to conclude that all the mappings that are needed have least fixed points.

This approach had the advantage of internalizing the proof that all mappings had least fixed points within the denotational setting. Roscoe's initial approach relied on a particularly involved proof using an associated operational model and a full abstraction theorem to reach this conclusion.

Since working with Roscoe and Schneider, I have pursued the theory of local cpos further. The results were presented at MFPS in 1995, and they showed how to construct a cartesian closed category of local cpos and monotone mappings all guaranteed to have least fixed points, and that allows models for unbounded analogues for two of the three power domains. What remains to be resolved is the question of the unbounded analogue to the Plotkin or convex power domain, a result that is under current study.

This gives some idea of the areas of interest that I have. All of them have many interesting, open problems that it would be useful to have solved. Domain theory, for example, and its extensions enjoy numerous areas of application and the problems these areas raise are a continuing source of new issues that need to be confronted. As one example, I would point to the work of Edalat mentioned earlier. His work has utilized the so-called Plotkin-Jones probabilistic power domain, and there now are emerging many new problems as researchers seek to understand better this construction and its potential application areas. --------------17AC72E81A9C--