Combining Higher-Order & First-Order Computation Using $\rho$-calculus: Towards a semantics of ELAN Full-version
Résumé
The recently introduced $\rho$-calculus permits to express in a uniform and simple way first-order rewriting, $\lambda$-calculus and non-deterministic computations as well as their combination. In this work, we emphasize the expressiveness of $\rho$-calculus and we give a full first-order presentation of this rewriting calculus using an explicit substitution setting $\rho\sigma$ that generalizes the $\lambda\sigma$-calculus. Its basic properties in the untyped as well as typed cases are presented. We then detail how to use the $\rho$-calculus to give an operational semantics to the rewrite based language Elan.