The Polymorphic Rewriting Calculus: Type checking vs. Type inferenceReportar como inadecuado

The Polymorphic Rewriting Calculus: Type checking vs. Type inference - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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 2 LOGNET - Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems CRISAM - Inria Sophia Antipolis - Méditerranée 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.

en fr

Keywords : polymorphism rewriting calculus type inference

Mots-clés : polymorphisme vérification de type inférence de type type checking calcul de réécriture pattern matching filtrage

Autor: Luigi Liquori - Benjamin Wack -



Documentos relacionados