Institutional Repository
| Polymorphic functions with set-theoretic types - Part 1: Syntax, semantics, and evaluation | |
| Castagna, Giuseppe (1); Nguyen, Kim (2); Xu, Zhiwu (1); Im, Hyeonseung (2); Lenglet, Sergueï (4); Padovani, Luca (5) | |
| 2014 | |
| Conference Name | 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 |
| Pages | 5-17 |
| Conference Date | January 22, 2014 - January 24, 2014 |
| Conference Place | San Diego, CA, United states |
| Indexed Type | SCI ; CPCI ; EI |
| Publish Place | Association for Computing Machinery, General Post Office, P.O. Box 30777, NY 10087-0777, United States |
| ISSN | 7308566 |
| ISBN | 9781450325448 |
| Department | (1) CNRS, PPS, Univ. Paris Diderot, Paris, France; (2) LRI, Université Paris-Sud, Orsay, France; (3) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (4) LORIA, Université de Lorraine, Nancy, France; (5) Dipartimento di Informatica, Università di Torino, Italy |
| English Abstract | This article is the first part of a two articles series about a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). In this first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed λ-calculus with intersection types and an efficient evaluation model for it. In the second part, presented in a companion paper, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations. The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data. © 2014 ACM.; This article is the first part of a two articles series about a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). In this first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed λ-calculus with intersection types and an efficient evaluation model for it. In the second part, presented in a companion paper, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations. The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data. © 2014 ACM. |
| Keyword | Types Polymorphism Xml Intersection Types |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16519 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Castagna, Giuseppe ,Nguyen, Kim ,Xu, Zhiwu ,et al. Polymorphic functions with set-theoretic types - Part 1: Syntax, semantics, and evaluation[C]. Association for Computing Machinery, General Post Office, P.O. Box 30777, NY 10087-0777, United States,2014:5-17. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment