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 metadatas

https://hal.inria.fr/inria-00099052
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:48:35 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM
Long-term archiving on : Wednesday, March 29, 2017 - 12:47:36 PM

Identifiers

  • HAL Id : inria-00099052, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

99

Files downloads

64