ELAN
The ELAN system provides an environment for specifying and prototyping deduction systems in a language based on rules controlled by strategies. Its purpose is to support the design of theorem provers, logic programming languages, constraints solvers and decision procedures and to offer a modular framework for studying their combination. Its purpose is to support the design of theorem provers, logic programming languages, constraints solvers and decision procedures and to offer a modular framework for studying their combination. ELAN takes from functional programming the concept of abstract data types and the function evaluation principle based on rewriting. But rewriting is inherently non-deterministic since several rules can be applied at different positions in a same term, and in ELAN, a computation may have several results. This aspect is taken into account through choice operations and a backtracking capability. One of the main originality of the language is to provide strategy constructors to specify whether a function call returns several, at-least one or only one result. This declarative handling of non-determinism is part of a strategy language allowing the programmer to specify the control on rules application. This is in contrast to many existing rewriting-based languages where the term reduction strategy is hard-wired and not accessible to the designer of an application. The strategy language offers primitives for sequential composition, iteration, deterministic and non-deterministic choices of elementary strategies that are labelled rules. From these primitives, more complex strategies can be expressed. In addition the user can introduce new strategy operators and define them by rewrite rules. Evaluation of strategy application is itself based on rewriting. So the simple and well-known paradigm of rewriting provides both the logical framework in which deduction systems can be expressed and combined, and the evaluation mechanism of the language. The purpose of these pages is to summarize ELAN features, library and environment and to provide a guide to the literature on the language.
Keywords for this software
References in zbMATH (referenced in 100 articles , 2 standard articles )
Showing results 1 to 20 of 100.
Sorted by year (- Fernández, Maribel; Kirchner, Hélène; Pinaud, Bruno: Strategic port graph rewriting: an interactive modelling framework (2019)
- Fernández, Maribel; Kirchner, Hélène; Pinaud, Bruno; Vallet, Jason: Labelled graph strategic rewriting for social networks (2018)
- Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors (2018)
- Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
- Fernández, Maribel; Kirchner, Hélène; Pinaud, Bruno; Vallet, Jason: Labelled graph rewriting meets social networks (2016)
- Ciobanu, Gabriel; Koutny, Maciej; Steggles, Jason: Strategy based semantics for mobility with time and access permissions (2015)
- Gutiérrez, Raúl; Lucas, Salvador: Function calls at frozen positions in termination of context-sensitive rewriting (2015)
- Kirchner, Hélene: Rewriting strategies and strategic rewrite programs (2015)
- López Bóbeda, Edmundo; Colange, Maximilien; Buchs, Didier: Stratagem: a generic Petri net verification framework (2014) ioport
- Baldan, Paolo; Bertolissi, Clara: Sharing in the graph rewriting calculus (2012)
- Gnaedig, Isabelle; Kirchner, Hélène: Proving weak properties of rewriting (2011)
- Alpuente, M.; Ballis, D.; Correa, F.; Falaschi, M.: An integrated framework for the diagnosis and correction of rule-based programs (2010)
- Shankar, Natarajan: Rewriting, inference, and proof (2010)
- Şerbănuţă, Traian Florin; Roşu, Grigore; Meseguer, José: A rewriting logic approach to operational semantics (2009)
- Brabrand, Claus; Schwartzbach, Michael I.: The metafront system: safe and extensible parsing and transformation (2007)
- Cirstea, Horatiu; Faure, Germain; Kirchner, Claude: A (\rho)-calculus of explicit constraint application (2007)
- Erwig, Martin; Ren, Deling: An update calculus for expressing type-safe program updates (2007)
- Faure, Germain: Term collections in (\lambda) and (\rho)-calculi (2007)
- Winter, Victor L.: Model-driven transformation-based generation of Java stress tests (2007) ioport
- Conchon, Sylvain; Krstić, Sava: Strategies for combining decision procedures (2006)