John McCarthy - US grants

This research into automatic theorem proving, program verification and mechanization of mathematical reasoning will be carried out over a period of three years. The basis is the study of logical formalisms for program verification and mathematical reasoning. This includes metamathematical reasoning and the proof checker (implemented at Stanford under NSF grant MCS-8206565) intensional semantics of programming languages and use of theorem proving tools to formalize semantics as a basis for proving intensional and extensional properties of programs and for mechanizing (aspects of) programming activities such as specification, transformation, and modification. the formalisms under study will be implemented using a common software platform. This software will be formally specified and proved to meet its specifications by the techniques to be investigated under the grant.

This investigation will use the variable type framework developed by Feferman to formalize programming in-the-large and to study alternatives to existing type systems, taking advantage of the rich type definition mechanisms provided by the variable type systems. The logical system will be enriched to explore its potential as a formal specification language and to accommodate even richer programming language constructs, including imperative features. This research will seek to provide new insights on the nature of types and specifications that can be used in the design of programming and specification languages and to develop tools for programming in- the-large. These insights will provide a basis for more effective use of formal methods in software design, development, and evolution.

Very little work has been done on the nature of program equivalence for typed higher-order languages with imperative features. In this project, investigations will continue into reasoning about programs with side-effects and other imperative features such as control abstractions. In particular, the semantics of various typed lambda calculi with references or pointers will be investigated. Simple types will be studied initially and a variety of extensions including polymorphism, effect systems, and control abstractions will then be explored. One aim of the research is to develop calculi of constrained equivalence which take into consideration the fact that a program or expression will only be used in certain contexts. In addition, the problem of providing for object-oriented programming in typed languages will be studied. This includes specifying classes of objects and defining notions of equivalence for objects and specifications of classes. This work can be seen from two points of view. First as studying typed fragments of untyped languages, axiomatizing program equivalence relative to a set of typed contexts and developing formal mechanisms for embedding typed fragments in untyped languages. Second as adding reference types and other imperative features and studying the effect of these additions on various type systems and on the nature of program equivalence.

This award will support collaborative research in "New Foundations of Computer Science" between Professor John McCarthy, Stanford University, and Professor Masahiko Sato, Tohoku University, Sendai, Japan, and several of their colleagues in the United States and Japan. The purpose of the collaboration is to advance the understanding of mathematical foundations of computer science. There is need to bring together mathematical tools that have been developed in basic research in computer science, to obtain a better understanding of these tools, and to develop new tools for studying foundational issues. Fundamental issues such as abstract and special purpose logics, mechanized reasoning systems, and abstract descriptions of programming constructs are among the topics where progress can be expected from the cooperative effort. Progress in these areas of basic research can have important consequences in areas such as computer architectures, languages, and systems, as well as in artificial intelligence and logic. The study of logics for computation, mechanized reasoning systems, and theory of programming languages is a very rapidly growing field. The U.S. and Japanese researchers taking part in this joint effort have substantial expertise in the areas of logic, formal reasoning, and mathematics as well as experience in the application of this expertise to a wide range of basic problems in computer science. Previous interaction among several of the scientists has been productive. This current cooperative endeavor will provide an opportunity to discover new foundational methods and to apply existing methods to current problems of artificial intelligence and programming language theory.

Distributed programs are complex and hard to reason about. An important source of difficulty in actual installed distribution systems is their open-ended nature; unlike modules described in traditional programming languages, over time distributed components may be added or removed, and they may change their connectivity. The goal of this project is to study how large systems can be divided into extensible modular components about which one can reason separately. Such a separation will facilitate the development and incremental modification of code. The research is based on a model of Actors: The model supports data encapsulation, procedural abstraction, asynchronous communication, reconfigurability, and dynamic creation. A formal algebra of actor configurations will be developed and methods for composing properties of open actor systems will be studied. The proposed research will provide a foundation for the formal verification of safety-critical distributed software systems.

The objective of this research is to develop a semantic foundation for semantic composition and interoperation of heterogeneous components of open systems. Composition and interoperation occur at many levels (requirements, specification, code, executables) and along multiple dimensions (functionality, reliability, security, availability). Relations among the various levels and dimensions must be preserved. Existing work on composition and interoperation has largely focused on syntactic structure. It is essential to develop a semantic basis in order to provide for safe, secure, and meaningful combinations. Semantic structuring of complex systems should provide a firm basis for determining what parts are interchangeable under given conditions, and to predict effects of changes: of components on the whole, and of system requirements on requirements for the parts. There is a wide range of applications where such a semantic foundation for interoperation can be of value. It is especially important in applications that combine components from diverse domains such as: data bases, spread sheets, knowledge bases, multi-media, mobile-agents, control theory, or event-based simulations. Metalogical methods from the theory of general logics, and associated techniques of mappings in and across formalisms, are used to achieve formalism-independent semantics for system composition. This supports the multi-dimensionality of a system's levels of description and formalization. Techniques from the theory of Open Mechanized Reasoning Systems (OMRS) as well as work on the formal semantics of actor systems are used to study interoperation aspects. Reflective techniques, particularly reflective logics and multi-model systems are employed extensively. This research is expected to lead to a new technology for composition, interoperation and dynamic evolution of software systems. It seeks to treat interoperability at many levels and along many dimensions: components, languages, speci fications, formalisms/logics, and tools. This provides the capacity to move in a mathematically rigorous way across the different formalizations of a system, and to use the different tools supporting these formalizations in a rigorously integrated way. The research is based on two key technical ideas: module calculi (for integration) and open multi-model systems (for interoperation). The module calculus is formalism-independent, and is intended to have powerful new operations such as generalization. Open multi-model systems formalize the multidimensional aspects of independent interoperating parts. ***

9900326 John McCarthy and Carolyn Talcott
Large software systems are increasingly complex and costly. The design, development, and maintenance of a system can be greatly helped by good documentation of its architecture, that is, of how it is structured into meaningful subsystems or components, and how those subsystems are glued together to form the overall system. A key unresolved problem is the interoperability problem, namely, how the architectural pieces and their multiple and possibly heterogeneous semantic descriptions corresponding to the different views fit together to make a coherent whole, and how these different descriptions impose constraints on each other. The main objectives of this collaborative project are (1) developing mathematical foundations for integrating and interoperating in a coherent and mathematically rigorous way diverse architectural descriptions, formal specifications, and executable prototypes of object-based distributed systems and (2) based on such foundations, developing a methodology for system design, development, and evolution that supports a seamless integration of the different formal and informal system descriptions and makes explicit the constraints that these different views of a system impose on each other. The development of mathematical foundations will be driven by substantial case studies and will begin with an in-depth study of a wide range of notations and formalisms and of their mutual relationships that seem particularly promising for describing systems at different levels. Rewriting logic will play an important role, not only as an executable specification formalism, but also as a reflective metalogical framework in which the chosen formalisms and their relations can be formalized. These formalizations can be executed using the meta tools developed in the Maude
language, an implementation of rewriting logic. It is expected that these foundations and experimental methodology will advance the state of the art in software development and evolution, and will lead to new tools and methods that, when used properly, will substantially reduce the cost and effort of software development and maintenance.

The Directorate of Social, Behavioral and Economic Sciences offers postdoctoral research fellowships to provide opportunities for recent doctoral graduates to obtain additional training, to gain research experience under the sponsorship of established scientists, and to broaden their scientific horizons beyond their undergraduate and graduate training. Postdoctoral fellowships are further designed to assist new scientists to direct their research efforts across traditional disciplinary lines and to avail themselves of unique research resources, sites, and facilities, including at foreign locations. This postdoctoral fellowship supports a rising scientist in the interdisciplinary area overlapping behavioral science, computational modeling and functional magnetic resonance imaging (fMRI), focusing on the process of decision making. Decision-making is a pervasive part of everyday life: in some cases, decisions are irreversible and in others an initial choice can be altered by a change of mind. For instance, when fetching a book off the shelf, one may initially reach toward the wrong title and later adjust the course of their reach in favor of the desired option. Such decisions require precise coordination between several brain systems to allocate attention, select a course of action, and execute hand and eye movements. Importantly, recent research demonstrates that cognition is tightly integrated with perception and action. Specifically, motor areas supporting the execution of eye and hand movements are also critically involved in decision-making; however, while the neural networks of decision-making are relatively well characterized, little is known about how the brain supports online changes to behavior after a decision to act has been executed. This proposal aims to investigate the brain systems supporting the ability to continuously modify decisions during target selection and determine how competition for attentional resources impacts this process. The results of this project will advance our understanding of the brain structures and neural information flow underlying rapid, flexible decision-making during action execution. This has important implications for informing impairments caused by disorders such as traumatic brain injury, stroke, and optic ataxia and the design of more advanced neural prosthetics to better serve amputees in dynamic, real-life settings.

The goal of this research is to provide a more comprehensive understanding of human decision-making by examining how multiple brain systems interact to support changes of mind during target selection. Using a multi-faceted approach including behavioral, electroencephalography (EEG), functional magnetic resonance imaging (fMRI), and advanced computational modeling techniques, this proposal will investigate the neural substrates that support rapid decision adjustments when executing actions. Specifically, how does the allocation of spatial attention during target selection impact change of mind? Moreover, what is the nature of information flow between higher-order cortical regions and eye- and hand-related motor areas during changes of mind during target selection? These results will represent an important step toward a more complete understanding of the brain mechanisms involved in complex human decision-making in naturalistic settings. This proposal is also supported by the NSF EPSCoR.