SRI International, Indiana University, University of Texas, University of Illinois, Johns Hopkins, University of Oregon, University of Copenhagen, Aarhus University, University of Pisa, University of Rome, University of Genova, IRST (Trento Italy), INRIA (Roquencourt, France), Tohoku University (Sendai Japan), Univeristy of Tokyo, NTT Labs, Tokyo, Imperial College (London), Queensland University, University of New England, University of Madrid, University of Freiburg, Korean Advanced Institue for Science and Technology (KAIST), Oregon Graduate Institute, Kestrel Institute, University of Maryland, Rensselaer Polytechnical Institute.
Workshop on Functional and Logic Programming, Trento Italy, 1986 Dagstuhl 1993 (Semantics and Specification), Dagstuhl 1995 (Interoperation and Coordingation), Semantique meeting, Aarhus Dk 1994 Workshop on Higher-Order Operational Techniques, 1995 IMACS Session for New Math in CS 1994, Semiotic Conference Session for New Math in CS 1996, MUDSHOP 1997, Brazil-Us Joint Workshop on Formal Foundations of Software Systems, Theoretical Aspects of Computer Software 1997, Dagstuhl 1998 (Information Systems as Reactive Systems), Reflections -in Honor of Solomon Feferman, 1998, Dagstuhl 2000 (Semi-Formal and Formal Specification Techniques for Software), Proofs for Mobility 2001 (ETAPS workshop), Formal Methods for Object-oriented Distributed Systems (FMOODS 2002), International Lisp Conference, 2002.
Ian Mason (*), Marianne Baudinet, Louis Galbiati, Alexandre Bronstein (*), Karen Myers, Gian Luigi Bellin, Erik Ruf, Elizabeth Wolf, Morry Katz, David Cyrluk (*) (Stanford), Anna Patterson, Nalini Venkatrasubramanian, Mark Astley, Prasanna Thati (U. Illinois).
Sandeep Uttamchandani (U. Illinois).
Karsten Gomard (DIKU), Lars Olsen Anderson (Masters - DIKU), Paolo di Blasio (U. Roma), Greg Sullivan (Northeastern), Manuel Clavel (Univeristy of Navarre), S¬oren Lassen (Aarhus University), Carlos H. C. Duarte (Imperial College, University of London).
My research interests derive from an interest in formal reasoning. Specific interests include semantics of higherorder programs with effects; formal modeling and analysis of distributed systems; and foundations of first-order reasoning. Methods I have developed for reasoning about imperative, functional, and concurrent programs are now being used by several research groups in the United States, Europe, and Australia.
In [talcott-96hoots-book] I introduced the notion of uniform semantics for imperative functional programs, providing general conditions for a context lemma introduced in [mason-talcott-89icalp] and establishing a basis for a programming logic [mason-talcott-00feferman]. In collaboration with Professors Agha, Mason, and Smith, I developed a formal theory of components of open distributed systems based on the actor model of computation.
In [talcott-96fmoods] two important notions are introduced: actor theories (called abstract actor structures in early papers) and interaction semantics. Interaction semantics abstracts away from the details of internal computation and provides a means of reasoning about actor system components considered as black boxes.
In collaboration with Prof. Venkatasubramanian at UC Irvine, I developed the TLAM reflective actor model for specifying and reasoning about composable middleware services in open distributed systems. The TLAM framework has been applied to a number of substantial case studies including distributed garbage collection [venk-agha-talcott-92iwmm, venk-talcott-95podc] and QoS-based multimedia service [venk-agha-talcott-01fme].
In collaboration with Prof. Smith of Johns Hopkins University, I developed a graphical notation for specification of actor system components called Specification Diagrams [smith-talcott-99fmoods, smith-talcott-02hosc]. This notation is similar in spirit to some of the event/message diagram notations of UML, and has a rigorous semantic foundation for composition, transformation, and checking satisfaction.
In collaboration with Prof. José Meseguer and others I have carried out substantial case studies developing formal models of network protocols and languages [denker-etal-99allerton, denker-meseguer-talcott-00disex, meseguer-olveczky-stehr-talcott-02dance, olveczky-etal-01fase, stehr-talcott-02wrla]. Meseguer and I have developed a model of distributedd object reflection [meseguer-talcott-02ecoop] that is being used in ongoing projects.
Currently I am using the Maude rewriting logic environment to develop and analyze executable formal models of a variety of systems, including: secure mobile agent systems [talcott-lincoln-03hcss], autonomous goal-oriented agents [denker-talcott-04wrla], and signal transduction systems in biological cells [eker-etal-02wrla, eker-etal-03csmb, talcott-etal-04psb].