Rewriting Calculus with(out) Types

8 years 12 months ago
Rewriting Calculus with(out) Types
The last few years have seen the development of a new calculus which can be considered as an outcome of the last decade of various researches on (higher order) term rewriting systems, and lambda calculi. In the Rewriting Calculus (or Rho Calculus, Cal), algebraic rules are considered as sophisticated forms of "lambda terms with patterns", and rule applications as lambda applications with pattern matching facilities. The calculus can be customized to work modulo sophisticated theories, like commutativity, associativity, associativity-commutativity, etc. This allows us to encode complex structures such as list, sets, and more generally objects. The calculus can either be presented "`a la Curry" or "`a la Church" without sacrificing readability and without complicating too much the metatheory. Many static type systems can be easily plugged-in on top of the calculus in the spirit of the rich typeoriented literature. The Rewriting Calculus could represent a li...
Horatiu Cirstea, Claude Kirchner, Luigi Liquori
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2002
Authors Horatiu Cirstea, Claude Kirchner, Luigi Liquori
Comments (0)