Navegar

Colección

Datos Estadísticas

Conferencia

Edi, J.; Viso, A.; Bonelli, E.; Uustalu T.; European Regional Development Fund "Ecient type checking for path polymorphism" (2018) 21st International Conference on Types for Proofs and Programs, TYPES 2015. 69:61-623
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that can operate uniformly over recursively specified applicative data structures. A typical pattern such functions resort to is xy which decomposes a compound, in other words any applicative tree structure, into its parts. We study type-checking for this type system in two stages. First we propose algorithms for checking type equivalence and subtyping based on coinductive characterizations of those relations. We then formulate a syntax-directed presentation and prove its equivalence with the original one. This yields a type-checking algorithm which unfortunately has exponential time complexity in the worst case. A second algorithm is then proposed, based on automata techniques, which yields a polynomial-time type-checking algorithm. © Juan Edi, Andrés Viso, and Eduardo Bonelli; licensed under Creative Commons License CC-BY 21st International Conference on Types for Proofs and Programs (TYPES 2015).

Registro:

Documento: Conferencia
Título:Ecient type checking for path polymorphism
Autor:Edi, J.; Viso, A.; Bonelli, E.; Uustalu T.; European Regional Development Fund
Filiación:Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Pabellón I, Ciudad Universitaria, Buenos Aires, C1428EGA, Argentina
Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET), Argentina and Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Pabellón I, Ciudad Universitaria, Buenos Aires, C1428EGA, Argentina
Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET), Argentina and Departamento de Ciencia y Tecnología, Universidad Nacional de Quilmes, Roque Sáenz Peña 352, Bernal, B1876BXD, Argentina
Palabras clave:Path polymorphism; Pattern matching; Type checking; Λ-calculus; Calculations; Differentiation (calculus); Pattern matching; Polynomial approximation; Trees (mathematics); Exponential time complexity; Polynomial-time; Recursive types; Tree structures; Type equivalence; Type systems; Typechecking; Typical patterns; Computer programming languages
Año:2018
Volumen:69
Página de inicio:61
Página de fin:623
DOI: http://dx.doi.org/10.4230/LIPIcs.TYPES.2015.6
Título revista:21st International Conference on Types for Proofs and Programs, TYPES 2015
Título revista abreviado:Leibniz Int. Proc. Informatics, LIPIcs
ISSN:18688969
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_18688969_v69_n_p61_Edi

Referencias:

  • Amadio, R.M., Cardelli, L., Subtyping recursive types (1993) ACM Trans. Program. Lang. Syst., 15 (4), pp. 575-631
  • Barendregt, H., Dekkers, W., Statman, R., Lambda calculus with types (2013) Perspectives in Logic, , Cambridge University Press
  • Brandt, M., Henglein, F., Coinductive axiomatization of recursive type equality and subtyping (1998) Fundam. Inf., 33 (4), pp. 309-338
  • Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A., An extension of system F with subtyping (1991) Theoretical Aspects of Computer Software, International Conference TACS'91, Sendai, Japan, September 24-27, 1991, Proceedings, Volume 526 of Lecture Notes in Computer Science, pp. 750-770. , In Takayasu Ito and Albert R. Meyer, editors, Springer
  • Colazzo, D., Ghelli, G., Subtyping recursion and parametric polymorphism in kernel Fun (2005) Inf. Comput., 198 (2), pp. 71-147
  • Cosmo, R.D., Pottier, F., Rémy, D., Subtyping recursive types modulo associative commutative products (2005) Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, Volume 3461 of Lecture Notes in Computer Science, pp. 179-193. , In Pawel Urzyczyn, editor, Springer
  • Downey, P.J., Sethi, R., Tarjan, R.E., Variations on the common subex-pression problem (1980) J. ACM, 27 (4), pp. 758-771
  • Edi, J., Viso, A., Prototype Implementation of E Cient Type-Checker in Scala, , https://github.com/juanedi/cap-typechecking, URL
  • Edi, J., Viso, A., Bonelli, E., (2017) E Cient Type Checking for Path Polymorphism, , http://arxiv.org/abs/1704.09026, URL
  • Jay, B., Kesner, D., First-class patterns (2009) J. Funct. Program., 19 (2), pp. 191-225
  • Jay, B., (2009) Pattern Calculus - Computing with Functions and Structures, , Springer
  • Jim, T., Palsberg, J., Type inference in systems of recursive types with subtyping (1999) Draft, , http://web.cs.ucla.edu/~palsberg/draft/jim-palsberg99.pdf, URL
  • Klop, J.W., Van Oostrom, V., Roel, C.D.V., Lambda calculus with patterns (2008) Theor. Comput. Sci., 398 (1-3), pp. 16-31
  • Kozen, D., Palsberg, J., Schwartzbach, M.I., E cient recursive subtyping (1995) Math. Struct. Comput. Sci., 5 (1), pp. 113-125
  • Palsberg, J., Zhao, T., E cient and flexible matching of recursive types (2001) Inf. Comput., 171 (2), pp. 364-387
  • Pierce, B.C., (2002) Types and Programming Languages, , MIT Press
  • Van Oostrom, V., (1990) Lambda Calculus with Patterns, , http://www.phil.uu.nl/~oostrom/publication/pdf/IR-228.pdf, Technical Report IR-228, Vrije Uni-versiteit Amsterdam, URL
  • Viso, A., Bonelli, E., Ayala-Rincón, M., Type soundness for path polymorphism (2016) Electr. Notes Theor. Comput. Sci., 323, pp. 235-251
  • Vouillon, J., Subtyping union types (2004) Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of The EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, Volume 3210 of Lecture Notes in Computer Science, pp. 415-429. , Jerzy Marcinkowski and Andrzej Tarlecki, editors, Springer
  • Zhao, T., (2002) Type Matching and Type Inference for Object-Oriented Systems, , http://docs.lib.purdue.edu/dissertations/AAI3099873/, PhD thesis, Purdue University, URLA4 - European Regional Development Fund

Citas:

---------- APA ----------
Edi, J., Viso, A., Bonelli, E., Uustalu T. & European Regional Development Fund (2018) . Ecient type checking for path polymorphism. 21st International Conference on Types for Proofs and Programs, TYPES 2015, 69, 61-623.
http://dx.doi.org/10.4230/LIPIcs.TYPES.2015.6
---------- CHICAGO ----------
Edi, J., Viso, A., Bonelli, E., Uustalu T., European Regional Development Fund "Ecient type checking for path polymorphism" . 21st International Conference on Types for Proofs and Programs, TYPES 2015 69 (2018) : 61-623.
http://dx.doi.org/10.4230/LIPIcs.TYPES.2015.6
---------- MLA ----------
Edi, J., Viso, A., Bonelli, E., Uustalu T., European Regional Development Fund "Ecient type checking for path polymorphism" . 21st International Conference on Types for Proofs and Programs, TYPES 2015, vol. 69, 2018, pp. 61-623.
http://dx.doi.org/10.4230/LIPIcs.TYPES.2015.6
---------- VANCOUVER ----------
Edi, J., Viso, A., Bonelli, E., Uustalu T., European Regional Development Fund Ecient type checking for path polymorphism. Leibniz Int. Proc. Informatics, LIPIcs. 2018;69:61-623.
http://dx.doi.org/10.4230/LIPIcs.TYPES.2015.6