The Polymorphic Rewriting Calculus: Type checking vs. Type inference
| Autor: | Liquori, Luigi, Wack, Benjamin |
|---|---|
| Přispěvatelé: | Objects, types and prototypes : semantics and validation (MIRHO), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems (LOGNET), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Narciso Marti-Oliet, Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo |
| Jazyk: | angličtina |
| Rok vydání: | 2004 |
| Předmět: |
Pattern-matching
type inference [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] vérification de type [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] polymorphisme [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] polymorphism TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES type checking pattern matching TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION inférence de type Type-checking vs. Type-inference Rewriting-calculus Computer Science::Programming Languages rewriting calculus calcul de réécriture filtrage |
| Zdroj: | Electronic Notes in Theoretical Computer Science Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004) Rewriting Logic and Its Applications 2004 Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004) Rewriting Logic and Its Applications 2004, Narciso Marti-Oliet, Mar 2004, Barcelona, Spain. pp.89-111, ⟨10.1016/j.entcs.2004.06.027⟩ |
| DOI: | 10.1016/j.entcs.2004.06.027⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|