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
|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.