A datalog solver based on rewriting logic.
Narrowing is a generalization of term rewriting that allows free variables in terms (as in logic programming) and replaces pattern matching by unification in order to (non-deterministically) reduce these terms. Narrowing was originally introduced as a mechanism for solving equational unification problems and then generalized to solve the more general problem of symbolic reachability. The narrowing mechanism has a number of important applications including automated proofs of termination, execution of functional-logic programming languages, partial evaluation, verification of cryptographic protocols, symbolic model checking, and equational unification.
A search command based on narrowing and a narrowing-based unification command for symbols with associativity, commutativity, and identity have been included in Full Maude. Details on their features and syntax, as well as several examples, are available in the Maude Manual.
Full Maude is available at the Maude site maude.cs.uiuc.edu/download and the latest version is always available at www.lcc.uma.es/~duran/FullMaude.
An automatic prover of narrowing termination.
A static program analyzer based on transforming Datalog query evaluation into parameterised boolean equation system resolution.
A Partial Evaluator for Functional Logic Programs
The FLIP system is an application that implements a framework for the Induction of Functional Logic Programs (IFLP).
A declarative debugger for functional logic programs.
A prototype system for the analysis and elimination of redundant arguments in functions.
A machine learning system that integrates many different features from other machine learning techniques and paradigms and, more importantly, it presents several innovations in many of these features.
An abstract diagnosis based debugger for functional programs.
A ``natural rewriting and narrowing'' prototype interpreter
which
improves (weakly) outermost-needed rewriting
and (weakly) outermost-needed narrowing
for non-inductively sequential CSs.
"VErification and Rewriting for Debugging Internet Sites", which is a system prototype being able to detect missing as well as incomplete Web pages w.r.t. a given formal specification.
New
rewriting-based Web verification service based on the system Verdi.
It is able to detect incorrect/forbidden information as well as
incomplete/missing Web pages in a Web site w.r.t a given formal
specification.
A machine
learning algorithm for inferring distance-based decision trees.
A prototype Haskell interpreter of [Alpuente et al. LPAR02] on-demand evaluation strategy.
An Incremental Curry Interpreter with polymorphic types and monadic declarative I/O
Here you can find an example Curry program which simulates the ecological behavior of the Segura river's basin. A description of this application (in spanish) can be found here.This is a purely declarative partial evaluator written in Curry itself. In contrast to INDY, it is able to deal with all the features of a modern functional logic language by translating source programs into the intermediate language FlatCurry
A Transformation System for Functional Logic Programs Based on Needed Narrowing. A graphic interface for SYNTH is available here
Two main features characterize our profiler: Our scheme is defined for the source language; hence, the attribution of costs to the user's program is straightforward. The profiler is "symbolic"; this means that it is independent of a particular implementation of the language. We do not return actual execution times but a list of symbolic measures: the number of computation steps, the number of allocated cells, the number of nondeterministic branches, and the number of pattern matching operations.
This is an extension of the partial evaluator above which incorporates the computation of symbolic costs. It also includes a simple speedup analysis which allows us to determine the concrete improvement achieved by the specialization process.
By exploting the similarities between (forward) slicing and (online) partial evaluation, we developed a forward slicing tool for Curry. The (forward) slicing tool has been implemented by adapting the partial evaluator above. It required a small implementation effort, i.e., only the underlying meta-interpreter needed significant changes.
The system implements source-to-source transformations for improving the efficiency of list-processing functions in Curry programs. In particular, we consider two list-processing optimizations which are fully automatic: an adaptation of the short cut deforestation (from functional programming) and a technique to introduce accumulating parameters (inspired by the logic programming difference-list transformation).
A compiler for FlatCurry programs into C++ based on memoization.
| ELP | GPLIS | DSIC | UPV |