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 |
| 会议名称 | 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 |
| 会议日期 | January 22, 2014 - January 24, 2014 |
| 会议地点 | San Diego, CA, United states |
| 关键词 | Types polymorphism XML intersection types |
| 页码 | 5-17 |
| 中文摘要 | 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. |
| 收录类别 | SCI ; CPCI ; EI |
| 会议录出版地 | Association for Computing Machinery, General Post Office, P.O. Box 30777, NY 10087-0777, United States |
| 语种 | 英语 |
| ISSN号 | 7308566 |
| ISBN号 | 9781450325448 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16519]  |
| 专题 | 软件研究所_软件所图书馆_会议论文 |
| 推荐引用方式 GB/T 7714 | Castagna, Giuseppe ,Nguyen, Kim ,Xu, Zhiwu ,et al. Polymorphic functions with set-theoretic types - Part 1: Syntax, semantics, and evaluation[C]. 见:41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014. San Diego, CA, United states. January 22, 2014 - January 24, 2014. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。