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
2 LOGNET - Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems
CRISAM - Inria Sophia Antipolis - Méditerranée
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.
Document type :
Conference papers
Complete list of metadatas

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 : Monday, November 5, 2018 - 3:36:03 PM
Long-term archiving on: Friday, April 2, 2010 - 7:49:02 PM

Files

cirstea.pdf

Identifiers

  • HAL Id : inria-00000817, version 1

Collections

INRIA | CNRS | I3S | UNICE | LORIA | UNIV-LORRAINE | UNIV-COTEDAZUR

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. pp.57-69. ⟨inria-00000817⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

367

Files downloads

118

 

 

Contact

archive-ouverte@inria.fr