PPDP

This paper summarises roughly ten years of experience using declarative programming for developing tools to validate formal specifications. More precisely, we present insights gained and lessons learned while implementing animators and model checkers in ...

The timed concurrent constraint programing model (tcc) is a declarative framework, closely related to First-Order Linear Temporal Logic (FLTL), for modeling reactive systems. The universal tcc formalism (utcc) is an extension of tcc with the ability to ...

Multi-set constraint rewriting allows for a highly parallel computational model and has been used in a multitude of application domains such as constraint solving, agent specification etc. Rewriting steps can be applied simultaneously as long as they do ...

In this paper we study, in the context of a WAM-based abstract machine for Prolog, how variations in the encoding of type information in tagged words and in their associated basic operations impact performance and memory usage.We use a high-level ...

Galculator is the name of the prototype of a proof assistant of a special brand: it is solely based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections ...

Workflow systems coordinate tasks of humans and computers. The iTask system is a recently developed toolkit with which workflows can be defined declaratively on a very high level of abstraction. It offers functionality which cannot be found in ...

This paper presents a new program analysis framework to approximate call patterns and their results in functional logic computations. We consider programs containing nonstrict, nondeterministic operations in order to make the analysis applicable to ...

In this paper, we study characterizations of polynomial complexity classes using first order functional programs and we try to improve their intensionality, that is the number of natural algorithms captured. We use polynomial assignments over the reals. ...

We propose to use the Knaster-Tarski least fixed point theorem as a basis to define recursive functions in the Calculus of Inductive Constructions. This widens the class of functions that can be modelled in type-theory based theorem proving tools to ...

We propose a paradigmatic programming language (called SlPCF) which is linear in a semantic sense. SlPCF is not syntactically linear, namely its programs can contain more than one occurrencies of the same variable. We give an interpretation of SlPCF ...

Types (or sorts) are pervasive in computer science and in rewritingbased programming languages, which often support subtypes (subsorts) and subtype polymorphism. Programs in these languages can be modeled as order-sorted term rewriting systems (OS-TRSs)...

Current parser generators are based on context-free grammars. Because such grammars lack abstraction facilities, the resulting specifications are often not easy to read. Fischer's macro grammars extend context-free grammars with macro-like productions ...

We present Pattern-by-Example (PBE), a graphical language that allows users with little or no knowledge of pattern-matching and functional programming to define complex and optimized queries on XML documents. We demonstrate the key features of PBE by ...

We present a new analysis that infers polymorphic type dependencies in logic programs. The analysis infers more precise information than previous type dependency inference analyses. The improvement in precision is achieved by making use of set union as ...

We present a destruction-aware type system for the functional language Safe, which is a first-order eager language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the ...

This paper explores a new point in the design space of functional programming: functional programming with dependently-typed higher-order data structures described in the logical framework LF. This allows us to program with proofs as higher-order data. ...

Abstract machines provide a certain separation between platform-dependent and platform-independent concerns in compilation. Many of the differences between architectures are encapsulated in the specific abstract machine implementation and the bytecode ...

Similarity-based Logic Programming (briefly, SLP) has been proposed to enhance the LP paradigm with a kind of approximate reasoning which supports flexible information retrieval applications. This approach uses a fuzzy similarity relation ℝ between ...

We define and examine six classes of methods for integrity checking: case-based, compositional, relevance-based, simplification-based, total-integrity-dependent, and measure-based ones. Each, except the penultimate, corresponds to a particular form of ...

Algorithmic debuggers for higher-order functional languages have to display functional values. Originally functional values had been represented as partial applications of function and constructor symbols, but a recent approach represents functional ...

In large, and often distributed, environments, where access control information may be shared across multiple sites, the combination of individual specifications in order to define a coherent access control policy is of fundamental importance. In order ...

Difference constraints of the form x - y ≤ d are well studied, with efficient algorithms for satisfaction and implication, because of their connection to shortest paths. Finite domain propagation algorithms however do not make use of these algorithms, ...

Constraint programming can definitely be seen as a model-driven paradigm. The users write programs for modeling problems. These programs are mapped to executable models to calculate the solutions. This paper focuses on efficient model management (...

Constraint propagation solvers interleave propagation (removing impossible values from variables domains) with search. Propagation is performed by executing propagators (removing values) implementing constraints (defining impossible values). In order to ...

This paper presents a computational model for the cooperation of constraint domains, based on a generic Constraint Functional Logic Programming (CFLP) Scheme and designed to support declarative programming with functions, predicates and the cooperation ...