Software Developed by S. Escobar


  • Narrowing in Maude

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

  • Maude-NPA

    • Maude-NPA is an analysis tool for cryptographic protocols that takes into account many of the algebraic properties of cryptosystems that are not included in other tools. These include cancellation of encryption and decryption, Abelian groups (including exclusive-or), and exponentiation. Maude-NPA uses an approach similar to the original NRL Protocol Analyzer; it is based on unification, and performs backwards search from a final state to determine whether or not it is reachable. Unlike the original NPA, it has a theoretical basis in rewriting logic and narrowing, and offers support for a wider basis of equational theories that includes associative-commutative (AC) theories.

  • UPV-Curry

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

  • An Automatic Useless Argument Elimination System

    • A prototype system for the analysis and elimination of redundant arguments in functions.

  • An implementation of on-demand strategy annotations

    • A prototype Haskell interpreter of [Alpuente et al. LPAR02] on-demand evaluation strategy.

  • Debussy

    • An abstract diagnosis based debugger for functional programs.

  • Natur

    • A ``natural rewriting and narrowing'' prototype interpreter which improves (weakly) outermost-needed rewriting and (weakly) outermost-needed narrowing for non-inductively sequential CSs.

  • Tools for the reflective programming language Maude:

    • Normalization via layered-normalization (new command "norm")

    • Normalization via program transformation (new command "eval")

    • On-demand evaluation (redefinition of command "red")

    • Normalization for on-demand evaluation via layered-normalization (redefinition of command "norm")

    © Copyright

    Unless otherwise noted, we hold copyright in all materials created by us, and allow general use under the ``copyleft'' terms of the GNU General Public License for software and the Open Content License for text. Essentially, you may use our copyright materials freely as long as you acknowledge our authorship and copyright. You may create variant and derivative works as long as you are accurate in attributing our contribution. You may redistribute our work, variants, and derivatives as long as you pass on the full license that we grant to you with every copy.