Polymorphic functions with set-theoretic types - Part 1: Syntax, semantics, and evaluation

ISCAS OpenIR

	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
页码	5-17
会议日期	January 22, 2014 - January 24, 2014
会议地点	San Diego, CA, United states
收录类别	SCI ; CPCI ; EI
出版地	Association for Computing Machinery, General Post Office, P.O. Box 30777, NY 10087-0777, United States
ISSN	7308566
ISBN	9781450325448
部门归属	(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
摘要	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.
关键词	Types Polymorphism Xml Intersection Types
语种	英语
内容类型	会议论文
URI标识	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]. Association for Computing Machinery, General Post Office, P.O. Box 30777, NY 10087-0777, United States,2014:5-17.