A *citizens' assembly* is a group of people who are randomly selected to represent a larger population in a deliberation. While this approach has successfully strengthened democracy, it has certain limitations that suggest the need for assemblies to form and associate more organically. In response, we propose *federated assemblies*, where assemblies are interconnected, and each parent assembly is selected from members of its child assemblies. The main technical challenge is to develop random selection algorithms that meet new representation constraints inherent in this hierarchical structure. We design and analyze several algorithms that provide different representation guarantees under various assumptions on the structure of the underlying graph.

Recent research in consensus has often focussed on protocols for State-Machine-Replication (SMR) that can handle high throughputs. Such state-of-the-art protocols (generally DAG-based) induce undue overhead when the needed throughput is low, or else exhibit unnecessarily-poor latency and communication complexity during periods of low throughput. Here we present Morpheus Consensus, which naturally morphs from a quiescent low-throughput leaderless blockchain protocol to a high-throughput leader-based DAG protocol and back, excelling in latency and complexity in both settings. During high-throughout, Morpheus pars with state-of-the-art DAG-based protocols, including Autobahn. During low-throughput, Morpheus exhibits competitive complexity and lower latency than standard protocols such as PBFT and Tendermint, which in turn do not perform well during high-throughput. The key idea of Morpheus is that as long as blocks do not conflict (due to Byzantine behaviour, network delays, or high-throughput simultaneous production) it produces a forkless blockchain, promptly finalizing each block upon arrival. It assigns a leader only if one is needed to resolve conflicts, in a manner and with performance not unlike Autobahn.

Cordial Miners are a family of efficient Byzantine Atomic Broadcast protocols, with instances for asynchrony and eventual synchrony. They improve the latency of state-of-the-art DAG-based protocols by almost 2X and achieve optimal good-case complexity of O(n) by forgoing Reliable Broadcast as a building block. Rather, Cordial Miners use the blocklace -- a partially-ordered counterpart of the totally-ordered blockchain data structure -- to implement the three algorithmic components of consensus: Dissemination, equivocation-exclusion, and ordering.

Informally, a distributed system is grassroots if it is permissionless and can have autonomous, independently-deployed instances - geographically and over time - that may interoperate voluntarily once interconnected. More formally, in a grassroots system the set of all correct behaviors of a set of agents P is strictly included in the set of the correct behaviors of P when they are embedded within a larger set of agents P' ⊃ P. Grassroots systems are potentially important as they may allow communities to conduct their social, economic, civic, and political lives in the digital realm solely using their members' networked computing devices (e.g., smartphones), free of third-party control, surveillance, manipulation, coercion, or rent seeking (e.g., by global digital platforms such as Facebook or Bitcoin). Client-server/cloud computing systems are not grassroots, and neither are systems designed to have a single global instance (Bitcoin/Ethereum with hardwired seed miners/bootnodes), and systems that rely on a single global data structure (IPFS, DHTs). An example grassroots system would be a serverless smartphone-based social network supporting multiple independently-budding communities that can merge when a member of one community becomes also a member of another. Here, we formalize the notion of grassroots distributed systems; describe a grassroots dissemination protocol for the model of asynchrony and argue its safety, liveness, and being grassroots; extend the implementation to mobile (address-changing) devices that communicate via an unreliable network (e.g. smartphones using UDP); and discuss how grassroots dissemination can realize grassroots social networking and grassroots cryptocurrencies. The mathematical construction employs distributed multiagent transition systems to define the notions of grassroots protocols, to specify the grassroots dissemination protocols, and to prove their correctness. The protocols use the blocklace - a distributed, partially-ordered counterpart of the replicated, totally-ordered blockchain.

Mainstream cryptocurrencies, based on proof of work or stake, require paying miners for the capital-intensive execution of a consensus protocol, and hence are unsuitable as a foundation for capital-free digital communities and for the bootstrap of a grassroots digital society. We aim to adapt and adjust the concepts, tools and technologies developed by the cryptocurrencies ecosystem, together with related networking technologies, into a foundation for a healthy grassroots digital economy and society. In this context we present the design and proof-of-concept implementation of a self-sovereign digital agent (ssDA), as an essential building block for a grassroots digital economy and society. The ssDA serves as a party, on behalf of its sovereign—a person—in digital social contracts, which are smart contracts among vetted participants, who are its sovereign in that they jointly execute the contract with an egalitarian consensus protocol. Digital social contracts may realize social networks, sharing economy applications, social governance of a digital community, and more. The ssDA is a software application that allows a person to partake in multiple digital social contracts simultaneously. Participation in a contract can be realized by initiating it or by being invited to it. Extra confidence in the integrity of the data is achieved by each person maintaining a blockchain containing all the person’s transactions in all contracts.

We study a setting in which a community wishes to identify a strongly supported proposal from a large space of alternatives, in order to change the status quo. We describe a deliberation process in which agents dynamically form coalitions around proposals that they prefer over the status quo. We formulate conditions on the space of proposals and on the ways in which coalitions are formed that guarantee deliberation to succeed, that is, to terminate by identifying a proposal with the largest possible support. Our results provide theoretical foundations for the analysis of deliberative processes in systems for democratic deliberation support, such as, e.g., LiquidFeedback or Polis.

We present a unifying framework encompassing a plethora of social choice settings. Viewing each social choice setting as voting in a suitable metric space, we offer a general model of social choice over metric spaces, in which—similarly to the spatial model of elections—each voter specifies an ideal element of the metric space. The ideal element acts as a vote, where each voter prefers elements that are closer to her ideal element. But it also acts as a proposal, thus making all participants equal not only as voters but also as proposers. We consider Condorcet aggregation and a continuum of solution concepts, ranging from minimizing the sum of distances to minimizing the maximum distance. We study applications of our abstract model to various social choice settings, including single-winner elections, committee elections, participatory budgeting, and participatory legislation. For each setting, we compare each solution concept to known voting rules and study various properties of the resulting voting rules. Our framework provides expressive aggregation for a broad range of social choice settings while remaining simple for voters; and may enable a unified and integrated implementation for all these settings, as well as unified extensions such as sybil-resiliency, proxy voting, and deliberative decision making. We study applications of our abstract model to various social choice settings, including single-winner elections, committee elections, participatory budgeting, and participatory legislation. For each setting, we compare each solution concept to known voting rules and study various properties of the resulting voting rules. Our framework provides expressive aggregation for a broad range of social choice settings while remaining simple for voters; and may enable a unified and integrated implementation for all these settings, as well as unified extensions such as sybil-resiliency, proxy voting, and deliberative decision making.

Preventing fake or duplicate digital identities (akasybils) from joining a digital community may be crucial to its survival, especially if it utilizes a consensus protocol among its members or employs democratic governance, where sybils can undermine consensus, tilt decisions, or even take over. Here, we explore the use of a trust-graph of identities, with edges representing trust among identity owners, to allow a community to grow indefinitely without increasing its sybil penetration. Since identities are admitted to the digital community based on their trust by existing digital community members,corruptidentities, which may trust sybils, also pose a threat to the digital community. Sybils and their corrupt perpetrators are together referred to asbyzantines, and the overarching aim is to limit their penetration into a digital community. We propose two alternative tools to achieve this goal. One is graph conductance, which works under the assumption that honest people are averse to corrupt ones and tend to distrust them. The second is vertex expansion, which relies on the assumption that there are not too many corrupt identities in the community. Of particular interest is keeping the fraction of byzantines below one third, as it would allow the use of Byzantine Agreement (Lamportet al., 1982) for consensus as well as for sybil-resilient social choice (Shahafet al., 2019). This paper considers incrementally growing a trust graph and shows that, under its key assumptions and additional requirements, including keeping the conductance or vertex expansion of the community trust graph sufficiently high, a community may grow safely, indefinitely.

Sybil attacks, in which fake or duplicate identities (a.k.a., Sybils) infiltrate an online community, pose a serious threat to such communities, as they might tilt community-wide decisions in their favor. While the extensive research on sybil identification may help keep the fraction of sybils in such communities low, it cannot however ensure their complete eradication. Thus, our goal here is to enhance social choice theory with effective group decision mechanisms for communities with bounded sybil penetration. Inspired by Reality-Aware Social Choice, we use the status quo as the anchor of Sybil Resilience, characterized by Sybil Safety -- the inability of sybils to change the status quo against the will of the genuine agents, and Sybil Liveness -- the ability of the genuine agents to change the status quo against the will of the sybils. We consider the social choice settings of deciding on a single proposal, on multiple proposals, and on updating a parameter. For each, we present social choice rules that are sybil-safe and, under certain conditions, satisfy sybil-liveness.

BACKGROUND: We have previously presented a formal language for describing population dynamics based on environment-dependent Stochastic Tree Grammars (eSTG). The language captures in broad terms the effect of the changing environment while abstracting away details on interaction among individuals. An eSTG program consists of a set of stochastic tree grammar transition rules that are context-free. Transition rule probabilities and rates, however, can depend on global parameters such as population size, generation count and elapsed time. In addition, each individual may have an internal state, which can change during transitions. RESULTS: This paper presents eSTGt (eSTG tool), an eSTG programming and simulation environment. When executing a program, the tool generates the corresponding lineage trees as well as the internal states values, which can then be analyzed either through the tool's GUI or using MATLAB's command-line environment. CONCLUSIONS: The presented tool allows researchers to use existing biological knowledge in order to model the dynamics of a developmental process and analyze its behavior throughout the historical events. Simulated lineage trees can be used to validate various hypotheses in silico and to predict the behavior of dynamical systems under various conditions. Written under MATLAB environment, the tool also enables to easily integrate the output data within the user's downstream analysis.

Advances in single-cell (SC) genomics enable commensurate improvements in methods for uncovering lineage relations among individual cells, as determined by phylogenetic analysis of the somatic mutations harbored by each cell. Theoretically, complete and accurate knowledge of the genome of each cell of an individual can produce an extremely accurate cell lineage tree of that individual. However, the reality of SC genomics is that such complete and accurate knowledge would be wanting, in quality and in quantity, for the foreseeable future. In this paper we offer a framework for systematically exploring the feasibility of answering cell lineage questions based on SC somatic mutational analysis, as a function of SC genomics data quality and quantity. We take into consideration the current limitations of SC genomics in terms of mutation data quality, most notably amplification bias and allele dropouts (ADO), as well as cost, which puts practical limits on mutation data quantity obtained from each cell as well as on cell sample density. We do so by generating in silico cell lineage trees using a dedicated formal language, eSTG, and show how the ability to answer correctly a cell lineage question depends on the quality and quantity of the SC mutation data. The presented framework can serve as a baseline for the potential of current SC genomics to unravel cell lineage dynamics, as well as the potential contributions of future advancement, both biochemical and computational, for the task.

BACKGROUND: Precise description of the dynamics of biological processes would enable the mathematical analysis and computational simulation of complex biological phenomena. Languages such as Chemical Reaction Networks and Process Algebras cater for the detailed description of interactions among individuals and for the simulation and analysis of ensuing behaviors of populations. However, often knowledge of such interactions is lacking or not available. Yet complete oblivion to the environment would make the description of any biological process vacuous. Here we present a language for describing population dynamics that abstracts away detailed interaction among individuals, yet captures in broad terms the effect of the changing environment, based on environment-dependent Stochastic Tree Grammars (eSTG). It is comprised of a set of stochastic tree grammar transition rules, which are context-free and as such abstract away specific interactions among individuals. Transition rule probabilities and rates, however, can depend on global parameters such as population size, generation count, and elapsed time. RESULTS: We show that eSTGs conveniently describe population dynamics at multiple levels including cellular dynamics, tissue development and niches of organisms. Notably, we show the utilization of eSTG for cases in which the dynamics is regulated by environmental factors, which affect the fate and rate of decisions of the different species. eSTGs are lineage grammars, in the sense that execution of an eSTG program generates the corresponding lineage trees, which can be used to analyze the evolutionary and developmental history of the biological system under investigation. These lineage trees contain a representation of the entire events history of the system, including the dynamics that led to the existing as well as to the extinct individuals. CONCLUSIONS: We conclude that our suggested formalism can be used to easily specify, simulate and analyze complex biological systems, and supports modular description of local biological dynamics that can be later used as "black boxes" in a larger scope, thus enabling a gradual and hierarchical definition and simulation of complex biological systems. The simple, yet robust formalism enables to target a broad class of stochastic dynamic behaviors, especially those that can be modeled using global environmental feedback regulation rather than direct interaction between individuals.

Organism cells proliferate and die to build, maintain, renew and repair it. The cellular history of an organism up to any point in time can be captured by a cell lineage tree in which vertices represent all organism cells, past and present, and directed edges represent progeny relations among them. The root represents the fertilized egg, and the leaves represent extant and dead cells. Somatic mutations accumulated during cell division endow each organism cell with a genomic signature that is unique with a very high probability. Distances between such genomic signatures can be used to reconstruct an organism's cell lineage tree. Cell populations possess unique features that are absent or rare in organism populations (e.g., the presence of stem cells and a small number of generations since the zygote) and do not undergo sexual reproduction, hence the reconstruction of cell lineage trees calls for careful examination and adaptation of the standard tools of population genetics. Our lab developed a method for reconstructing cell lineage trees by examining only mutations in highly variable microsatellite loci (MS, also called short tandem repeats, STR). In this study we use experimental data on somatic mutations in MS of individual cells in human and mice in order to validate and quantify the utility of known lineage tree reconstruction algorithms in this context. We employed extensive measurements of somatic mutations in individual cells which were isolated from healthy and diseased tissues of mice and humans. The validation was done by analyzing the ability to infer known and clear biological scenarios. In general, we found that if the biological scenario is simple, almost all algorithms tested can infer it. Another somewhat surprising conclusion is that the best algorithm among those tested is Neighbor Joining where the distance measure used is normalized absolute distance. We include our full dataset in Tables S1, S2, S3, S4, S5 to enable further analysis of this data by others.

Synaptic wiring of neurons in Caenorhabditis elegans is largely invariable between animals. It has been suggested that this feature stems from genetically encoded molecular markers that guide the neurons in the final stage of synaptic formation. Identifying these markers and unraveling the logic by which they direct synapse formation is a key challenge. Here, we address this task by constructing a probabilistic model that attempts to explain the neuronal connectivity diagram of C. elegans as a function of the expression patterns of its neurons. By only considering neuron pairs that are known to be connected by chemical or electrical synapses, we focus on the final stage of synapse formation, in which neurons identify their designated partners. Our results show that for many neurons the neuronal expression map of C. elegans can be used to accurately predict the subset of adjacent neurons that will be chosen as its postsynaptic partners. Notably, these predictions can be achieved using the expression patterns of only a small number of specific genes that interact in a combinatorial fashion.

The depth of a cell of a multicellular organism is the number of cell divisions it underwent since the zygote, and knowing this basic cell property would help address fundamental problems in several areas of biology. At present, the depths of the vast majority of human and mouse cell types are unknown. Here, we show a method for estimating the depth of a cell by analyzing somatic mutations in its microsatellites, and provide to our knowledge for the first time reliable depth estimates for several cells types in mice. According to our estimates, the average depth of oocytes is 29, consistent with previous estimates. The average depth of B cells ranges from 34 to 79, linearly related to the mouse age, suggesting a rate of one cell division per day. In contrast, various types of adult stem cells underwent on average fewer cell divisions, supporting the notion that adult stem cells are relatively quiescent. Our method for depth estimation opens a window for revealing tissue turnover rates in animals, including humans, which has important implications for our knowledge of the body under physiological and pathological conditions.

Trinucleotide hereditary diseases such as Huntington disease and Friedreich ataxia are cureless diseases associated with inheriting an abnormally large number of DNA trinucleotide repeats in a gene. The genes associated with different diseases are unrelated and harbor a trinucleotide repeat in different functional regions; therefore, it is striking that many of these diseases have similar correlations between their genotype, namely the number of inherited repeats and age of onset and progression phenotype. These correlations remain unexplained despite more than a decade of research. Although mechanisms have been proposed for several trinucleotide diseases, none of the proposals, being disease-specific, can account for the commonalities among these diseases. Here, we propose a universal mechanism in which length-dependent somatic repeat expansion occurs during the patient's lifetime toward a pathological threshold. Our mechanism uniformly explains for the first time to our knowledge the genotype-phenotype correlations common to trinucleotide disease and is well-supported by both experimental and clinical data. In addition, mathematical analysis of the mechanism provides simple explanations to a wide range of phenomena such as the exponential decrease of the age-of-onset curve, similar onset but faster progression in patients with Huntington disease with homozygous versus heterozygous mutation, and correlation of age of onset with length of the short allele but not with the long allele in Friedreich ataxia. If our proposed universal mechanism proves to be the core component of the actual mechanisms of specific trinucleotide diseases, it would open the search for a uniform treatment for all these diseases, possibly by delaying the somatic expansion process.

What is the lineage relation among the cells of an organism? The answer is sought by developmental biology, immunology, stem cell research, brain research, and cancer research, yet complete cell lineage trees have been reconstructed only for simple organisms such as Caenorhabditis elegans. We discovered that somatic mutations accumulated during normal development of a higher organism implicitly encode its entire cell lineage tree with very high precision. Our mathematical analysis of known mutation rates in microsatellites (MSs) shows that the entire cell lineage tree of a human embryo, or a mouse, in which no cell is a descendent of more than 40 divisions, can be reconstructed from information on somatic MS mutations alone with no errors, with probability greater than 99.95%. Analyzing all approximately 1.5 million MSs of each cell of an organism may not be practical at present, but we also show that in a genetically unstable organism, analyzing only a few hundred MSs may suffice to reconstruct portions of its cell lineage tree. We demonstrate the utility of the approach by reconstructing cell lineage trees from DNA samples of a human cell line displaying MS instability. Our discovery and its associated procedure, which we have automated, may point the way to a future "Human Cell Lineage Project" that would aim to resolve fundamental open questions in biology and medicine by reconstructing ever larger portions of the human cell lineage tree.

Although electronic computers are the only "computer species" we are accustomed to, the mathematical notion of a programmable computer has nothing to do with wires and logic gates. In fact, Alan Turing's notional computer, which marked in 1936 the birth of modern computer science and still stands at its heart, has greater similarity to natural biomolecular machines such as the ribosome and polymerases than to electronic computers. Recently, a new "computer species" made of biological molecules has emerged. These simple molecular computers inspired by the Turing machine, of which a trillion can fit into a microliter, do not compete with electronic computers in solving complex computational problems; their potential lies elsewhere. Their molecular scale and their ability to interact directly with the biochemical environment in which they operate suggest that in the future they may be the basis of a new kind of "smart drugs": molecular devices equipped with the medical knowledge to perform disease diagnosis and therapy inside the living body. They would detect and diagnose molecular disease symptoms and, when necessary, administer the requisite drug molecules to the cell, tissue or organ in which they operate. In the talk we review this new research direction and report on preliminary steps carried out in our lab towards realizing its vision.

Although electronic computers are the only species we are accustomed to, the mathematical notion of a programmablecomputer has nothing to do with wires and logic gates. In fact, Alan Turing's notional computer, which marked in 1936 the birth of modern computer science and still stands at its heart, has greater similarity to natural biomolecular machines such as the ribosome and polymerases than to electronic computers. Recently, a new species made of biological molecules has emerged. These simple molecular computers inspired by the Turing machine, of which a trillion can fit into a microliter, do not compete with electronic computers in solving complex computational problems; their potential lies elsewhere. Their molecular scale and their ability to interact directly with the biochemical environment in which they operate suggest that in the future they may be the basis of a new kind of smart drugs: molecular devices equipped with the medical knowledge to perform disease diagnosis and therapy inside the living body. They would detect and diagnose molecular disease symptoms and, when necessary, administer the requisite drug molecules to the cell, tissue or organ in which they operate. In the talk we review this new research direction and report on preliminary steps carried out in our lab towards realizing its vision.

Abstract Data Types (ADTs) has been introduced recently to Israeli high-school students as tools for problem solving and knowledge representation in Prolog environment. This paper reviews a research that was conducted in order to assess the influence of students' use of ADTs on the development process of knowledge-based Prolog programs.

No abstract available.

Article Active mail—a framework for implementing groupware Share on Authors: Yaron Goldberg View Profile , Marilyn Safran View Profile , Ehud Shapiro View Profile Authors Info & Claims CSCW '92: Proceedings of the 1992 ACM conference on Computer-supported cooperative workDecember 1992 Pages 75–83https://doi.org/10.1145/143457.143464Online:01 December 1992Publication History 35citation652DownloadsMetricsTotal Citations35Total Downloads652Last 12 Months5Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Optimistic type systems for logic programs are considered. In such systems types are conservative approximations to the success set of the program predicates. The use of logic programs to describe types is proposed. It is argued that this approach unifies the denotational and operational approaches to descriptive type systems and is simpler and more natural than previous approaches. The focus is on the use of unary-predicate programs to describe the types. A proper class of unary-predicate programs is identified, and it is shown that it is expensive enough to express several notions of types. An analogy with two-way automata and a correspondence with alternating algorithms are used to obtain a complexity characterization of type inference and type checking. This characterization is facilitated by the use of logic programs to represent types.>

The problem of replaying computations of nondeterministic concurrent programs arises in contexts such as debugging and recovery. We investigate the problem for an abstract model of concurrency, which generalizes dataflow networks, processors with shared variables, and logic programming models of concurrency. We say that nondeterminism is visible if the state is determined, up to some (appropriately defined) notion of equivalence, by the external behavior. We show that if nondeterminism is visible then replay is achievable using a one-step lookahead sequential simulation algorithm. If the program has an additional monotonicity property called stability then recovery is possible without simulating the original computation, by restarting the program from a certain easily constructed state. Also, for stable programs with visible nondeterminism, a process composed of identical parallel processes has the same external behavior as each of its components. Hence high crash-failure res...

Concurrent programming enjoys a proliferation of languages but suffers from the lack of a general method of language comparison. In particular, concurrent (as well as sequential) programming languages can-not be usefully distinguished based on complexity-theoretic considerations, since most of them are Turing-complete. Nevertheless, differences between program-ming languages matter, else we would not have invented so many of them. We develop a general method for comparing concur-rent programming languages based on their algebraic (structural) complexity, and, using this method, achieve separation results among many well-known concurrent languages. The method is not restricted to concurrent languages. It can be used to compare the algebraic complexity of abstract machine models, other families of programming languages, logics, and, more generaly, any family of lan-guages with some syntactic operations and a notion of semantic equivalence. The method can also be used to compare the algebraic complexity of families of opera-tions wit hin a language or across languages. We note that using the method we were able to compare lan-guages and computational models that do not have a common semantic basis.

Processes in concurrent logic programs communicate and synchronize using shared singleassignment variables.Communication is performed via unification operations, while synchronization is performed through input matching.The more expressive concurrent logic languages employ atomic unification as the basic communication primitive.Atomic unification can be thought of as an atomic transaction that either fails with no trace or succeeds in writing on all of the necessary writable variables occurring in the unification instance.This pa- per presents a distributed variable server algorithm that can be used as the key component in a distributed implementation of concurrent logic languages with atomic unification.The variable server provides an abstraction in which processes can act as if all of the shared variables are local.It thus allows programs to be written for a shared memory model and executed in a system in which memory is distributed.We rigorously specify the requirements the variable server must fulfill, present an algorithm satisfying the specification, and prove its correctness with respect to the specification.The algorithm has been implemented for the language Flat Concurrent Prolog (FCP) and is incorporated in the distributed version of the Logix system.

The authors develop a resolution logic that is based on direct proofs rather than on proofs by refutations. The deductive system studied has clauses as its formulas and resolution as the sole inference rule. They analyze this deductive system using a novel representation of resolution proofs, called resolution graphs, and obtain a general completeness theorem: a clause is a logical consequence of a set of clauses if and only if it is either tautological or subsumed by a clause derivable from that set. In a previous paper (proc. 16th ACM Symp. on Principles of Prog. Lang., pp.134-42, 1989), the authors developed a model-theoretic compositional semantics for logic programs and investigated the fully abstract equivalences induced by various notions of composition. They continue that study here using the proof theory of resolution logic. This proof theory gives rise to various semantics for logic programs that reflect more operational details than does the model-theoretic semantics.>

We propose a framework for discussing fully abstract compositional semantics, which exposes the interrelations between the choices of observables, compositions, and meanings. Every choice of observables and compositions determines a unique fully abstract equivalence. A semantics is fully abstract if it induces this equivalence.

A denotational, hence, compositional semantics for a subset of Concurrent Prolog is developed and related to an operational semantics. The denotational semantics makes divergence and the resultant substitutions of finite computations together with the termination mode-success, failure, or deadlock-observable. Relative to this notion of observation it is proved that the denotational semantics is fully abstract in the sense that it records the minimal amount of extra information beyond the observables to make it compositional. Full abstraction is an important property because it quantifies the information that one needs in order to reason about individual program-parts independently. This is believed to be the first such result in the area of concurrent logic programming.>

Concurrent Prolog [28] combines the logic programming computation model with guarded-command indeterminacy and dataflow synchronization. It will form the basis of the Kernel Language [21] of the Parallel Inference Machine [36], planned by Japan's Fifth Generation Computers Project. This paper explores the feasibility of programming such a machine solely in Concurrent Prolog (in the absence of a lower-level programming language), by implementing in it a representative collection of systems programming problems.

The notion of program correctness with respect to an interpretation is defined for a class of programming languages. Under this definition, if a program terminates with an incorrect output then it contains an incorrect procedure. Algorithms for detecting incorrect procedures are developed. These algorithms formalize what experienced programmers may know already.A logic program implementation of these algorithms is described. Its performance suggests that the algorithms can be the backbone of debugging aids that go far beyond what is offered by current programming environments.Applications of algorithmic debugging to automatic program construction are explored.