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 , 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.
Document type :
Conference papers
17è Journées Francophones des Langages Applicatifs - JFLA 2006, Jan 2006, Pauillac, France. INRIA, pp.57-69, 2006
Liste complète des métadonnées

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000817
Contributor : Benjamin Wack <>
Submitted on : Monday, December 12, 2005 - 3:59:40 PM
Last modification on : Tuesday, October 25, 2016 - 4:57:57 PM
Document(s) archivé(s) le : Friday, April 2, 2010 - 7:49:02 PM

Identifiers

  • HAL Id : inria-00000817, version 1

Collections

Citation

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. INRIA, pp.57-69, 2006. 〈inria-00000817〉

Share

Metrics

Record views

252

Document downloads

78