The simply typed rewriting calculus

The rewriting calculus is a rule construction and application framework. As such it embeds in a uniform way term rewriting and lambda-calculus. Since rule application is an explicit object of the calculus, it allows us also to handle the set of results explicitly. We present a simply typed version of the rewriting calculus. With a good choice of the type system, we show that the calculus is type preserving and terminating, i.e. verifies the subject reduction and strong normalization properties.

• Type: Journal
• Year: 2000
• Where: ENTCS
• Authors: Horatiu Cirstea, Claude Kirchner
• Keywords: ENTCS 2000, Rewriting Calculus, Rule Construction, Uniform Way Term