Navegar

Colección

Datos Estadísticas

Artículo

Viso, A.; Bonelli, E.; Ayala-Rincón, M. "Type Soundness for Path Polymorphism" (2016) Electronic Notes in Theoretical Computer Science. 323:235-251
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:

Path polymorphism is the ability to define functions that can operate uniformly over arbitrary recursively specified data structures. Its essence is captured by patterns of the form xy which decompose a compound data structure into its parts. Typing these kinds of patterns is challenging since the type of a compound should determine the type of its components. We propose a static type system (i.e. no run-time analysis) for a pattern calculus that captures this feature. Our solution combines type application, constants as types, union types and recursive types. We address the fundamental properties of Subject Reduction and Progress that guarantee a well-behaved dynamics. Both these results rely crucially on a notion of pattern compatibility and also on a coinductive characterisation of subtyping. © 2016 The Author(s)

Registro:

Documento: Artículo
Título:Type Soundness for Path Polymorphism
Autor:Viso, A.; Bonelli, E.; Ayala-Rincón, M.
Filiación:Consejo Nacional de Investigaciones Científicas y Técnicas – CONICET, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires – UBA, Buenos Aires, Argentina
Consejo Nacional de Investigaciones Científicas y Técnicas – CONICET, Departamento de Ciencia y Tecnología, Universidad Nacional de Quilmes – UNQ, Bernal, Argentina
Departamentos de Matemática e Ciência da Computação, Universidade de Brasília – UnB, Brasília D.F., Brazil
Palabras clave:Path Polymorphism; Pattern Matching; Static Typing; λ-Calculus; Data structures; Differentiation (calculus); Pattern matching; Compound data structure; Fundamental properties; Pattern calculus; Recursive types; Run-time analysis; Static type systems; Static typing; Subject reduction; Calculations
Año:2016
Volumen:323
Página de inicio:235
Página de fin:251
DOI: http://dx.doi.org/10.1016/j.entcs.2016.06.015
Título revista:Electronic Notes in Theoretical Computer Science
Título revista abreviado:Electron. Notes Theor. Comput. Sci.
ISSN:15710661
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15710661_v323_n_p235_Viso

Referencias:

  • Amadio, R.M., Cardelli, L., Subtyping recursive types (1993) ACM Trans. Program. Lang. Syst., 15, pp. 575-631
  • Arbiser, A., Miquel, A., Ríos, A., The lambda-calculus with constructors: Syntax, confluence and separation (2009) J. Funct. Program., 19, pp. 581-631
  • Ariola, Z.M., Klop, J.W., Equational term graph rewriting (1996) Fundam. Inform., 26, pp. 207-240
  • Lambda Calculus with Types (2013), Perspectives in Logic, in: H. Barendregt, W. Dekkers, R. Statman (Eds.), CUP; Barthe, G., Cirstea, H., Kirchner, C., Liquori, L., Pure patterns type systems (2003) Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 250-261. , http://doi.acm.org/10.1145/640128.604152, A. Aiken G. Morrisett New Orleans, Louisisana, USA, January 15–17, 2003
  • Brandt, M., Henglein, F., Coinductive axiomatization of recursive type equality and subtyping (1998) Fundam. Inform., 33, 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, LNCS, 526, pp. 750-770. , http://dx.doi.org/10.1007/3-540-54415-1_73, T. Ito A.R. Meyer Springer Berlin Heidelberg
  • Cardone, F., An algebraic approach to the interpretation of recursive types (1992) CAAP, LNCS, 581, pp. 66-85. , J.-C. Raoult
  • Cirstea, H., Kirchner, C., The rewriting calculus - part i and ii (2001) Logic Journal of the IGPL, 9, pp. 339-410
  • Cirstea, H., Kirchner, C., Liquori, L., Matching power (2001) Proceedings of the Rewriting Techniques and Applications, 12th International Conference, RTA 2001, LNCS, 2051, pp. 77-92. , http://dx.doi.org/10.1007/3-540-45127-7_8, A. Middeldorp Utrecht, The Netherlands, May 22–24, 2001
  • Cirstea, H., Kirchner, C., Liquori, L., The rho cube (2001) Proceedings of the Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 (ETAPS 2001), LNCS, 2030, pp. 168-183. , http://dx.doi.org/10.1007/3-540-45315-6_11, F. Honsell M. Miculan Genova, Italy, April 2-6, 2001
  • Cirstea, H., Kirchner, C., Liquori, L., Rewriting calculus with(out) types (2002) Electr. Notes Theor. Comput. Sci., 71, pp. 3-19
  • Cirstea, H., Liquori, L., Wack, B., Rewriting calculus with fixpoints: Untyped and first-order systems (2003) Types for Proofs and Programs, International Workshop, TYPES 2003, LNCS, 3085, pp. 147-161. , http://dx.doi.org/10.1007/978-3-540-24849-1_10, S. Berardi M. Coppo F. Damiani Torino, Italy, April 30 - May 4, 2003 Revised Selected Papers
  • Colazzo, D., Ghelli, G., Subtyping recursion and parametric polymorphism in kernel fun (2005) Information and Computation, 198, pp. 71-147. , http://www.sciencedirect.com/science/article/pii/S0890540105000167
  • Di Cosmo, R., Pottier, F., Rémy, D., Subtyping recursive types modulo associative commutative products (2005) Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, TLCA'05, pp. 179-193
  • Edi, J., Chequeo de tipos eficiente para Path Polymorphism (2015), Master's thesis Universidad de Buenos Aires Buenos Aires, Argentina; Jay, C.B., Pattern Calculus: Computing with Functions and Structures (2009), Springer; Jay, C.B., Kesner, D., Pure pattern calculus (2006) ESOP, LNCS, 3924, pp. 100-114. , P. Sestoft
  • Jay, C.B., Kesner, D., First-class patterns (2009) J. Funct. Program., 19, pp. 191-225
  • Jha, S., Palsberg, J., Zhao, T., Efficient type matching (2002) Proceedings of the Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002 (ETAPS 2002), LNCS, 2303, pp. 187-204. , http://dx.doi.org/10.1007/3-540-45931-6_14, M. Nielsen U. Engberg Grenoble, France, April 8–12, 2002
  • Kozen, D., Palsberg, J., Schwartzbach, M.I., Efficient recursive subtyping (1995) Mathematical Structures in Computer Science, 5, pp. 113-125
  • Liquori, L., Wack, B., The polymorphic rewriting-calculus: [type checking vs. type inference] (2005) Electr. Notes Theor. Comput. Sci., 117, pp. 89-111
  • Palsberg, J., Zhao, T., Efficient and flexible matching of recursive types (2001) Inf. Comput., 171, pp. 364-387
  • Petit, B., Semantics of typed lambda-calculus with constructors (2011) Logical Methods in Computer Science, 7
  • Pierce, B.C., Types and Programming Languages (2002), MIT Press Cambridge, MA, USA; ten Eikelder, H., Some algorithms to decide the equivalence of recursive types (1991), Technical Report 91/31 Eindhoven University of Technology; Viso, A., Bonelli, E., Ayala-Rincón, M., Type soundness for path polymorphism (2015), http://arxiv.org/abs/1601.03271, Extended report; Vouillon, J., Subtyping union types (2004) CSL, LNCS, 3210, pp. 415-429. , J. Marcinkowski A. Tarlecki

Citas:

---------- APA ----------
Viso, A., Bonelli, E. & Ayala-Rincón, M. (2016) . Type Soundness for Path Polymorphism. Electronic Notes in Theoretical Computer Science, 323, 235-251.
http://dx.doi.org/10.1016/j.entcs.2016.06.015
---------- CHICAGO ----------
Viso, A., Bonelli, E., Ayala-Rincón, M. "Type Soundness for Path Polymorphism" . Electronic Notes in Theoretical Computer Science 323 (2016) : 235-251.
http://dx.doi.org/10.1016/j.entcs.2016.06.015
---------- MLA ----------
Viso, A., Bonelli, E., Ayala-Rincón, M. "Type Soundness for Path Polymorphism" . Electronic Notes in Theoretical Computer Science, vol. 323, 2016, pp. 235-251.
http://dx.doi.org/10.1016/j.entcs.2016.06.015
---------- VANCOUVER ----------
Viso, A., Bonelli, E., Ayala-Rincón, M. Type Soundness for Path Polymorphism. Electron. Notes Theor. Comput. Sci. 2016;323:235-251.
http://dx.doi.org/10.1016/j.entcs.2016.06.015