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.
Type de document :
Communication dans un congrès
Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo. Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004) Rewriting Logic and Its Applications 2004, Mar 2004, Barcelona, Spain. Elsevier, Electronic Notes in Theoretical Computer Science, 117, pp.89-111, 2005, 〈10.1016/j.entcs.2004.06.027〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00099910
Contributeur : Luigi Liquori <>
Soumis le : jeudi 7 mai 2015 - 12:28:01
Dernière modification le : jeudi 11 janvier 2018 - 16:44:54
Document(s) archivé(s) le : mercredi 19 avril 2017 - 19:03:00

Fichier

2005-wrla-04.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Luigi Liquori, Benjamin Wack. The Polymorphic Rewriting Calculus: Type checking vs. Type inference. Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo. Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004) Rewriting Logic and Its Applications 2004, Mar 2004, Barcelona, Spain. Elsevier, Electronic Notes in Theoretical Computer Science, 117, pp.89-111, 2005, 〈10.1016/j.entcs.2004.06.027〉. 〈inria-00099910〉

Partager

Métriques

Consultations de la notice

95

Téléchargements de fichiers

52