Skip to Main content Skip to Navigation
Conference papers

Rewriting Calculus with Fixpoints: Untyped and First-order Systems

Horatiu Cirstea 1 Luigi Liquori 2, 3 Benjamin Wack 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 MIRHO - Objects, types and prototypes : semantics and validation
CRISAM - Inria Sophia Antipolis - Méditerranée , UHP - Université Henri Poincaré - Nancy 1, Université Nancy 2, INPL - Institut National Polytechnique de Lorraine, CNRS - Centre National de la Recherche Scientifique : UMR7503
Abstract : The rewriting calculus, also called ρ-calculus, is a framework embedding λ-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the λ-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the λ-calculus can be generalized to the ρ-calculus: in this paper, we study extensively a first-order ρ-calculus à la Church, called ρstk→ . The type system of ρstk→ allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language.
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00100113
Contributor : Luigi Liquori <>
Submitted on : Thursday, May 7, 2015 - 2:07:18 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Wednesday, April 19, 2017 - 7:02:11 PM

File

2004-types-03.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Horatiu Cirstea, Luigi Liquori, Benjamin Wack. Rewriting Calculus with Fixpoints: Untyped and First-order Systems. Types for Proofs and Programs International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, Apr 2003, Turin, Italy. pp.147-161, ⟨10.1007/978-3-540-24849-1_10⟩. ⟨inria-00100113⟩

Share

Metrics

Record views

408

Files downloads

315