Kim Marriott

LOPSTR Conference 2000 Conference Paper

A model for inter-module analysis and optimizing compilation

• Francisco Bueno
• Maria Garcia de la Banda
• Manuel V. Hermenegildo
• Kim Marriott
• Germán Puebla
• Peter J. Stuckey

TCS Journal 1997 Journal Article

A confluent calculus for concurrent constraint programming

• Kim Marriott
• Martin Odersky

Confluence is an important and desirable property as it allows the program to be understood by considering any desired scheduling rule, rather than having to consider all possible schedulings. Unfortunately, the usual operational semantics for concurrent constraint programs is not confluent as different process schedulings give rise to different sets of possible outcomes. We show that it is possible to give a natural confluent calculus for concurrent constraint programs, if the syntactic domain is extended by a blind choice operator and a special constant standing for a discarded branch. This has application to program analysis.

TCS Journal 1997 Journal Article

Confluence in concurrent constraint programming

• Moreno Falaschi
• Maurizio Gabbrielli
• Kim Marriott
• Catuscia Palamidessi

Concurrent constraint programming (ccp), like most of the concurrent paradigms, has a mechanism of global choice which makes computations dependent on the scheduling of processes. This is one of the main reasons why the formal semantics of ccp is more complicated than the one of its deterministic and local-choice sublanguages. In this paper we study various subsets of ccp obtained by adding some restriction on the notion of choice, or by requiring confluency, i. e. independency from the scheduling strategy. We show that it is possible to define simple denotational semantics for these subsets, for various notions of observables. Finally, as an application of our results we develop a framework for the compositional analysis of full ccp. The basic idea is to approximate an arbitrary ccp program by a program in the restricted language, and then analyze the latter, by applying the standard techniques of abstract interpretation to its denotational semantics.

I&C Journal 1997 Journal Article

Constraint Logic Programming with Dynamic Scheduling: A Semantics Based on Closure Operators

• Moreno Falaschi
• Maurizio Gabbrielli
• Kim Marriott
• Catuscia Palamidessi

The first logic programming languages, such as Prolog, used a fixed left-to-right atom scheduling rule. Recent logic programming languages, however, provide more flexible scheduling in which there is a default computation rule such as left-to-right but in which some calls are dynamically “delayed” until their arguments are sufficiently instantiated to allow the call to run efficiently. Such languages include constraint logic programming languages, since most implementations of these languages delay constraints which are “too hard. ” From the semantic point of view, the fact that an atom must be delayed under certain conditions, causes the standard semantics of (constraint) logic programming to be no longer adequate to capture the meaning of a program. In our paper we attack this problem and we develop a denotational semantics for constraint logic programming with dynamic scheduling. The key idea is that the denotation of an atom or goal is a set of closure operators, where different closure operators correspond to different sequences of rule choices.

TCS Journal 1996 Journal Article

Negative Boolean constraints

• Kim Marriott
• Martin Odersky

Systems of Boolean constraints which allow negative constraints such as f ⊊︀ g are investigated. The results form a basis for algorithms to determine satisfiability, validity, implication, equivalence and variable elimination for such systems. These algorithms have applications in spatial query decomposition, machine reasoning and constraint logic programming. Proofs of the results rely on independence of inequations, which enables results for systems with a single inequation to be lifted to systems with many inequations.

MFCS Conference 1991 Invited Paper

Elimination of Negation in Term Algebras

• Jean-Louis Lassez
• Michael J. Maher
• Kim Marriott

Abstract We give an informal review of the problem of eliminating negation in term algebras and its applications. The initial results appear to be very specialized with complex combinatorial proofs. Nevertheless they have applications and relevance to a number of important areas: unification, learning, abstract data types and rewriting systems, constraints and constructive negation in logic languages.