Skip to Main content Skip to Navigation
New interface
Conference papers

The simply typed rewriting calculus

Horatiu Cirstea 1 Claude Kirchner 1 
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:48:35 AM
Last modification on : Friday, February 4, 2022 - 3:22:47 AM
Long-term archiving on: : Wednesday, March 29, 2017 - 12:47:36 PM


  • HAL Id : inria-00099052, version 1



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⟩



Record views


Files downloads