List of Accepted Papers
| Manuel Montenegro, Ricardo Peña and Clara Segura. A Simple Region Inference Algorithm for a First-Order Functional Language |
| Abstract: Safe 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 heap, where the program allocates data structures. The runtime system does not need a garbage collector and all allocation/deallocation actions are done in constant time. The language is aimed at inferring and certifying upper bounds for memory consumption in a Proof Carrying Code environment. Some of its analyses have been presented elsewhere. In this paper we present an inference algorithm for annotating programs with regions which is both simpler to understand and more efficient than other related algorithms. Programmers are assumed to write programs and to declare datatypes without any reference to regions. The algorithm decides the regions needed by every function. It also allows polymorphic recursion with respect to regions. We show convincing examples of programs before and after region annotation, prove the correctness and optimality of the algorithm, and give its asymptotic cost. |
| Yuki Kato and Koji Nakazawa. Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types |
| Abstract: This paper shows that type-checking and type-inference problems are equivalent in domain-free lambda calculi with existential types, that is, type-checking problem is Turing reducible to type-inference problem and vice versa. A decision problem P is said to be Turing reducible to another problem Q when there is a computable function F such that for any instance p of P, F(p) is an instance of Q which holds if and only if p holds. In this paper, the equivalence is proved for two variants of domain-free lambda calculi with existential types: one is an implication and existence fragment, and the other is a negation, conjunction and existence fragment. Implication, negation, and conjunction in logic correspond to the functional type, the continuation type, and the product type, respectively. This result gives another proof of undecidability of type inference in the domain-free calculi with existence. |
| Petra Hofstedt and Kazunori Ueda. Realizing Multiparadigm Programming based on Hierarchical Graph Rewriting |
| Abstract: The paper presents the new multiparadigm programming language CCFL which allows the description of concurrent processes and of non-deterministic behavior and it discusses the compilation of CCFL programs into the hierarchical graph rewriting language LMNtal. LMNtal aims at the unification of paradigms of computation and supports by its features and structure the transformation of CCFL programs such that we reached clear and simple compilation schemata. |
| Rafael del Vado Vírseda and Ignacio Castiñeiras Pérez. A Theoretical Framework for the Declarative Debugging of Functional Logic Programs with Lambda Abstractions |
| Abstract: In this paper, we extend the declarative method for diagnosing wrong computed answers in first-order lazy functional logic programs to the higher-order setting of the simply typed lambda calculus, where programs are presented by conditional pattern rewrite systems. Our approach generalizes and combines declarative debugging techniques previously developed for less expressive declarative programming paradigms involving applicative rewrite rules instead of lambda abstractions and higher-order unification. Debugging starts with the observation of a wrong computed answer which the user regards as incorrect w.r.t. an intended model that provides a declarative description of the program's semantics. Debugging proceeds by exploring an abridged proof tree built on a higher-order rewriting logic with lambda abstractions that provides a purely declarative view of the computation. Finally, debugging ends with the detection of a defined function rule in the program that is incorrect w.r.t. the intended model. We prove the logical correctness of the debugging method for any sound goal solving system whose computed answers are logical consequences of the program. |
| Javier Álvez and Francisco Javier López-Fraguas. A Complete Axiomatization of Strict Equality over Infinite Trees |
| Abstract: Computing with data values that are some kind of trees ---finite, infinite, rational--- is at the core of declarative programming, either logic, functional or functional-logic. Understanding the logic of trees is therefore a fundamental question with impact in different aspects, like language design, including constraint systems or constructive negation, or obtaining methods for verifying and reasoning about programs. The theory of true equality over finite or infinite trees is quite well known. In particular, a seminal paper by Maher proved its decidability and gave a complete axiomatization of the theory. However, the sensible notion of equality for functional and functional-logic languages with a lazy evaluation regime is strict equality, a computable approximation to true equality for possibly infinite and partial trees. In this paper, we investigate the first order theory of strict equality, arriving to remarkable and not obvious results: the theory is again decidable and admits a complete axiomatization, not requiring predicate symbols other than strict equality itself. Besides, the results stem from an effective ---taking into account the intrinsic complexity of the problem--- decision procedure that can be seen as a constraint solver for general strict equality constraints. |
| Francisco Javier Lopez-Fraguas, Enrique Martin-Martin and Juan Rodriguez-Hortala. Advances in type systems for Functional-Logic Programming |
| Abstract: Type systems are widely used in programming languages as a powerful tool providing safety to programs, and forcing the programmers to write code in a clearer way. Functional-logic languages have inherited Damas & Milner type system from their functional part due to its simplicity and popularity. In this paper we address a couple of aspects that can be subject of improvement. One is related to a problematic feature of functional-logic languages not taken under consideration by standard systems: it is known that the use of opaque HO patterns in left-hand sides of program rules may produce undesirable effects from the point of view of types. We re-examine the problem, and propose a Damas & Milner-like type system where certain uses of HO patterns (even opaque) are permitted while preserving type safety, as proved by a subject reduction result that uses HO-let-rewriting, a recently proposed operational semantics for HO functional logic programs. At the same time that we formalize the type system, we have made the effort of technically clarifying additional issues: one is the different ways in which polymorphism of local definitions can be handled, and the other is the overall process of type inference in a whole program. |
| Nacho Castiñeiras and Fernando Sáenz. Integrating ILOG CP technology into TOY |
| Abstract: Currently, our constraint functional logic programming system TOY uses the SICStus Prolog finite domain (FD) constraint solver. In this work, we integrate the ILOG CP FD constraint solving technology into the system TOY , with the aim of improving its applicability. We describe our implementation of ILOG CP into TOY emphasizing the communication between them. Performance results are reported. |
| Michael Leuschel, Salvador Tamarit and German Vidal. Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation |
| Abstract: A logic program strongly terminates if it terminates for any selection rule. Clearly, considering a particular selection rule (like Prolog's leftmost selection rule) allows one to prove more goals terminating. In contrast, a strong termination analysis gives valuable information for those applications in which the selection rule cannot be fixed in advance (e.g., partial evaluation, dynamic selection rules, parallel execution). In this paper, we introduce a fast and accurate size-change analysis that can be used to infer conditions for both strong termination and quasi-termination of logic programs. In the paper we also provide several ways to increase the accuracy of the analysis without sacrificing scalability. In the experimental evaluation, we show that the new algorithm is up to three orders of magnitude faster than the previous implementation, meaning that we can efficiently deal with realistic programs exceeding 25,000 lines of Prolog. |
| Manuel Hernandez. A Taxonomy of Some Right-to-Left String-Matching Algorithms |
| Abstract: This work presents a taxonomy of some exact string-matching algorithms. The taxonomy is based on results obtained by using logic program transformation over an initial, naive and nondeterministic specification. The string-matching algorithms report whether a pattern occurs in a text by comparing character to character, from right to left, the pattern and a portion of the text. A derivation of the search part and some notes about the preprocessing part of each algorithm is presented. The derivations show several design decisions behind each algorithm, and allow us to organize the algorithms within a taxonomic tree, giving us a better understanding of these algorithms and possible mechanical procedures to derive them. |
| Makoto Hamana. Semantic Labelling for Proving Termination of Combinatory Reduction Systems |
| Abstract: We give a method of proving termination of higher-order rewrite rules in Klop's format combinatory reduction system (CRS). The format CRS essentially covers the usual pure higher-order functional programs such as Haskell. Our method to prove termination, called higher-order semantic labelling, is an extension of a method known in the theory of term rewriting. This attaches semantics of the arguments to each function symbol. We systematically define the labelling by using the complete algebraic semantics of CRS, \Sigma-monoids. We also examine the power of higher-order semantic labelling by several examples. This includes an interesting example from the viewpoint of functional programming and semantics; we show termination of the monad of the lambda terms. |
| Stephan Falke and Deepak Kapur. Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures |
| Abstract: Context-sensitive rewriting is a restriction of rewriting that can be used to elegantly model declarative specification and programming languages such as Maude. Furthermore, it can be used to model lazy evaluation in functional languages such as Haskell. Building upon our previous work on an expressive and elegant class of rewrite systems (called CERSs) that contains built-in numbers and supports the use of collection data structures such as sets or multisets, we consider context-sensitive rewriting with CERSs in this paper. This integration results in a natural way for specifying algorithms in the rewriting framework. In order to prove termination of this kind of rewriting automatically, we develop a dependency pair framework for context-sensitive rewriting with CERSs, resulting in a flexible termination method that can be automated effectively. Several powerful termination techniques are developed within this framework. An implementation in the termination prover AProVE has been successfully evaluated on a large collection of examples. |
| andre rauber du bois, gerson cavalheiro and juliana vizzotto. pFun: A semi-explicit parallel purely functional language |
| Abstract: In this paper we present the design and implementation of $p$Fun, a semi-explicit parallel purely functional language. Parallelism is introduced in $p$Fun through annotations. These annotations indicate expressions that can be evaluated in parallel with the rest of the program. Task creation, synchronization and scheduling of computations on processors are managed automatically by $p$Fun's runtime system. $p$Fun's programming model and runtime system are described, and preliminary measurements of the current prototype implementation on an SMP-machine, a Beowulf Cluster and an small heterogeneous GRID are presented. |