The simply typed rewriting calculus

Horatiu Cirstea (1) , Claude Kirchner (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

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.

Mots clés: type preserving; calcul de réécriture; rewriting calculus; type system; normalization; système de types; normalisation; préservation des types

Domaines: Autre [cs.OH]

Horatiu Cirstea, Claude Kirchner. The simply typed rewriting calculus. 3rd International Workshop on Rewriting Logic & its Applications - WRLA2000, Sep 2000, none, 19 p. ⟨inria-00099052⟩