LIPIcs.TYPES.2015.4.pdf
- Filesize: 0.71 MB
- 29 pages
Document
Constrained Polymorphic Types for a Calculus with Name Variables
Authors
-
Part of:
Volume:
21st International Conference on Types for Proofs and Programs (TYPES 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-03-15
Cite AsGet BibTex
Davide Ancona, Paola Giannini, and Elena Zucca. Constrained Polymorphic Types for a Calculus with Name Variables. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2015.4
https://doi.org/10.4230/LIPIcs.TYPES.2015.4
Abstract
We extend the simply-typed lambda-calculus with a mechanism for dynamic rebinding of code based on parametric nominal interfaces. That is, we introduce values which represent single fragments, or families of named fragments, of open code, where free variables are associated with names which do not obey \alpha-equivalence. In this way, code fragments can be passed as function arguments and manipulated, through their nominal interface, by operators such as rebinding, overriding and renaming. Moreover, by using name variables, it is possible to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly enhancing expressivity. However, in order to prevent conflicts when instantiating name variables, the name-polymorphic types of such terms need to be equipped with simple {inequality} constraints. We show soundness of the type system.
Keywords
- open code
- incremental rebinding
- name polymorphism
- metaprogramming
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- D. Ancona, P. Giannini, and E. Zucca. Reconciling positional and nominal binding. In S. Graham-Lengrand and L. Paolini, editors, Proc. of 6th Wksh. on Intersection Types and Related Systems, ITRS 2012, volume 121 of Electron. Proc. in Theor. Comput. Sci., pages 81-93. Open Publishing Assoc., 2013. URL: http://dx.doi.org/10.4204/eptcs.121.6.
- D. Ancona, P. Giannini, and E. Zucca. Type safe incremental rebinding. Math. Struct. Comput. Sci., 27(2):94-122, 2017. URL: http://dx.doi.org/10.1017/s0960129515000109.
- D. Ancona and E. Zucca. A calculus of module systems. J. Funct. Program., 12(2):91-132, 2002. URL: http://dx.doi.org/10.1017/s0956796801004257.
- Davide Ancona, Paola Giannini, and Elena Zucca. Incremental rebinding with name polymorphism. Electr. Notes Theor. Comput. Sci., 322:19-34, 2016. URL: http://dx.doi.org/10.1016/j.entcs.2016.03.003.
- Davide Ancona, Giovanni Lagorio, and Elena Zucca. Jam - designing a java extension with mixins. ACM Trans. Program. Lang. Syst., 25(5):641-712, 2003. URL: http://dx.doi.org/10.1145/937563.937567.
- Gavin M. Bierman, Michael W. Hicks, Peter Sewell, Gareth Paul Stoyle, and Keith Wansbrough. Dynamic rebinding for marshalling and update, with destruct-time? In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, pages 99-110. ACM, 2003. URL: http://dx.doi.org/10.1145/944705.944715.
- L. Dami. A lambda-calculus for dynamic binding. Theor. Comput. Sci., 192(2):201-231, 1997. URL: http://dx.doi.org/10.1016/s0304-3975(97)00150-3.
- M. Dezani-Ciancaglini, P. Giannini, and E. Zucca. Intersection types for unbind and rebind. In E. Pimentel, B. Venneri, and J. Wells, editors, Proc. of 5th Wksh. on Intersection Types and Related Systems, ITRS 2010, volume 45 of Electron. Proc. in Theor. Comput. Sci., pages 45-58. Open Publishing Assoc., 2011. URL: http://dx.doi.org/10.4204/eptcs.45.4.
- Mariangiola Dezani-Ciancaglini, Paola Giannini, and Elena Zucca. Extending the lambda-calculus with unbind and rebind. RAIRO - Theor. Inf. and Applic., 45(1):143-162, 2011. URL: http://dx.doi.org/10.1051/ita/2011008.
-
D. Flanagan. JavaScript: The Definitive Guide. O'Reilly, 4th edition, 2011.
- L. Moreau. A syntactic theory of dynamic binding. High. Order Symb. Comput., 11(3):233-279, 1998. URL: http://dx.doi.org/10.1023/a:1010087314987.
- Aleksandar Nanevski. From dynamic binding to state via modal possibility. In Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden, pages 207-218. ACM, 2003. URL: http://dx.doi.org/10.1145/888251.888271.
- A. M. Pitts and M. R. Shinwell. Generative unbinding of names. Log. Methods Comput. Sci., 4(1):article 4, 2008. URL: http://dx.doi.org/10.2168/lmcs-4(1:4)2008.
- Mark R. Shinwell, Andrew M. Pitts, and Murdoch Gabbay. Freshml: programming with binders made simple. In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, pages 263-274. ACM, 2003. URL: http://dx.doi.org/10.1145/944705.944729.
-
B. Stroustrup. The C++ Programming Language. Addison-Wesley, 4th edition, 2013.
- W. Taha and T. Sheard. MetaML and multi-stage programming with explicit annotations. Theor. Comput. Sci., 248(1-2):211-242, 2000. URL: http://dx.doi.org/10.1016/s0304-3975(00)00053-0.