PPDP

We present a technique for cryptographic protocol verification, based on an intermediate representation of the protocol by a set of Horn clauses (a logic program). This technique makes it possible to verify security properties of the protocols, such as ...

Trust management systems have been proposed as an alternative to traditional security mechanisms in Global Computing. We present some challenges in establishing a formal foundation for the notion of trust, and some preliminary ideas towards a category ...

We bridge the gap between functional evaluators and abstract machines for the λ-calculus, using closure conversion, transformation into continuation-passing style, and defunctionalization.We illustrate this approach by deriving Krivine's abstract ...

We present a new evaluation strategy for functional logic programs described by weakly orthogonal conditional term rewriting systems. Our notion of weakly orthogonal conditional rewrite system extends a notion of Bergstra and Klop and covers a large ...

An unsatisfiable set of constraints is minimal if all its (strict) subsets aresatisfiable.A number of forms of error diagnosis, including circuit error diagnosis and type error diagnosis, require finding all minimal unsatisfiable subsets of a given set ...

Language for Structured Design (LSD)is a high level, visual, logic programming language for design of structured objects. LSD combines the design and programming activities in a homogeneous programming/design environment by extending Lograph, a visual ...

ViMer is a visual debugging environment for Mercury programs which has three main contributions. First, it employs a new execution tree representation, the layered AND-OR tree, which we believe provides a better way of visualizing backtracking in AND-OR-...

We propose a rank 2 intersection type system for a language of modules built on a core ML-like language. The principal typing property of the rank 2 intersection type system for the core language plays a crucial role in the design of the type system for ...

Constraint Handling Rules (CHRs) are a high-level committed choice programming language commonly used to write constraint solvers. While the semantic basis of CHRs allows them to extend arbitrary underlying constraint solvers, in practice, all current ...

We propose a new algorithm of secrecy analysis in a framework integrating declarative programming and concurrency. The analysis of a program ensures that information can only flow from less sensitive levels toward more sensitive ones. Our algorithm uses ...

Starting from P. Sestoft semantics for lazy evaluation, we define a new semantics in which normal forms consist of variables pointing to lambdas or constructions. This is in accordance with the more recent changes in the Spineless Tagless G-machine (STG)...

Outermost-needed rewriting/narrowing is a sound and complete optimal demand-driven strategy for the class of inductively sequential constructor systems. Its parallel extension (known as weakly) deals with non-inductively sequential constructor systems. ...

In rule-based languages, control of rule application can be expressed thanks to strategy constructors. The paper addresses termination of such strategy-guided evaluation. To fix ideas, we use the ELAN strategy language. We first give a sufficient ...

In this paper we present a technique for the optimization of bound queries over disjunctive deductive databases with constraints. The proposed approach consists of two distinct phases: i) the rewriting of queries for propagating bindings from the query ...

We present an extension of first-order term rewriting systems, which involves variable binding in the term language. We develop the systems called binding term rewriting systems (BTRSs) in a stepwise manner; firstly we present the term language, then ...

This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than standard call-by-value recursive definitions. We ...

This paper describes a method for transforming any given set of Datalog rules into an efficient specialized implementation with guaranteed worst-case time and space complexities, and for computing the complexities from the rules. The running time is ...

We investigate a framework for representing and reasoning about syntactic and semantic aspects of typed languages with variable binders.First, we introduce typed binding signatures and develop a theory of typed abstract syntax with binders. Each ...

Substitution in the lambda calculus is a complex operation that traditional presentations of beta contraction naively treat as a unitary operation. Actual implementations are more careful. Within them, substitutions are realized incrementally through ...

In this paper we propose a typed, purely functional calculus for state (with second-class locations) in which types reflect the dichotomy between reading from and writing into the global store. This is in contrast to the usual formulation of state via ...

In this paper we propose a semantically well-founded combination of the constraint solvers used in the constraint programming languages CLP(SET) and CLP(FD). This work demonstrates that it is possible to provide efficient executions (through CLP(FD) ...

Non-strict purely functional languages pose many challenges to the designers of debugging tools. Declarative debugging has long been considered a suitable candidate for the task due to its abstraction over the evaluation order of the program, although ...

The standard formalism for explaining abstract types is existential quantification. While it provides a sufficient model for type abstraction in entirely statically typed languages, it proves to be too weak for languages enriched with forms of dynamic ...

We propose a demand-driven conditional narrowing calculus in which a variant of definitional trees [2] is used to efficiently control the narrowing strategy. This calculus is sound and strongly complete w.r.t. Constructor-based ReWriting Logic (CRWL) ...

Proof checkers for proof-carrying code (and similar systems) can suffer from two problems: huge proof witnesses and untrustworthy proof rules. No previous design has addressed both of these problems simultaneously. We show the theory, design, and ...

Early resolution mechanisms proposed for tabling such as OLDT rely on suspension and resumption of subgoals to compute fixpoints. Recently, a new resolution framework called linear tabling has emerged as an alternative tabling method. The idea of linear ...