Skip to Main content Skip to Navigation
Conference papers

The Polymorphic Rewriting Calculus: Type checking vs. Type inference

Luigi Liquori 1, 2 Benjamin Wack 3
1 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
3 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The rewriting calculus (rho-calculus), is a minimal framework embedding lambda-calculus and term rewriting systems, by allowing abstraction on variables and patterns. The rho-calculus features higher-order functions (from lambda-calculus) and pattern-matching (from term rewriting systems). In this paper, we study extensively a second-order rho-calculus à la Church (Rho F) that enjoys subject reduction, type uniqueness and decidability of typing. Then we apply a classical type-erasing function to rho 2, to obtain an untyped rho-calculus à la Curry (uRho F). The related type inference system is isomorphic to Rho F and enjoys subject reduction. Both Rho F and uRho F systems can be considered as minimal calculi for polymorphic rewriting-based programming languages. We discuss the possibility of a logic existing underneath the type systems via a Curry-Howard Isomorphism.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Thursday, May 7, 2015 - 12:28:01 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Wednesday, April 19, 2017 - 7:03:00 PM


Files produced by the author(s)




Luigi Liquori, Benjamin Wack. The Polymorphic Rewriting Calculus: Type checking vs. Type inference. Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004) Rewriting Logic and Its Applications 2004, Narciso Marti-Oliet, Mar 2004, Barcelona, Spain. pp.89-111, ⟨10.1016/j.entcs.2004.06.027⟩. ⟨inria-00099910⟩



Les métriques sont temporairement indisponibles