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
2 LOGNET - Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems
3 MASCOTTE - Algorithms, simulation, combinatorics and optimization for telecommunications

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.

Domaines: Algorithme et structure de données [cs.DS]; Langage de programmation [cs.PL]; Informatique et langage [cs.CL]; Logique en informatique [cs.LO]

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⟩