Decidable Type Inference for the Polymorphic Rewriting Calculus

Horatiu Cirstea 1 Claude Kirchner 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 MASCOTTE - Algorithms, simulation, combinatorics and optimization for telecommunications
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : The rewriting calculus is a minimal framework embedding lambda calculus and term rewriting systems that allows abstraction on variables and patterns. The rewriting calculus features higher-order functions (from the lambda calculus) and pattern matching (from term rewriting systems). In this paper, we study extensively the decidability of type inference in the second-order rewriting calculus à la Curry.
Liste complète des métadonnées

Cited literature [29 references]  Display  Hide  Download
Contributor : Benjamin Wack <>
Submitted on : Monday, December 12, 2005 - 3:59:40 PM
Last modification on : Monday, November 5, 2018 - 3:36:03 PM
Document(s) archivé(s) le : Friday, April 2, 2010 - 7:49:02 PM


  • HAL Id : inria-00000817, version 1


Horatiu Cirstea, Claude Kirchner, Luigi Liquori, Benjamin Wack. Decidable Type Inference for the Polymorphic Rewriting Calculus. 17è Journées Francophones des Langages Applicatifs - JFLA 2006, Jan 2006, Pauillac, France. pp.57-69. ⟨inria-00000817⟩



Record views


Files downloads