¶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 lambda-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.

¶BiBTex

@inproceedings{10.1145/2535838.2535840,
author = {Castagna, Giuseppe and Nguyen, Kim and Xu, Zhiwu and Im, Hyeonseung and Lenglet, Sergue\"{\i} and Padovani, Luca},
title = {Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation},
year = {2014},
isbn = {9781450325448},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2535838.2535840},
doi = {10.1145/2535838.2535840},
booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {5–17},
numpages = {13},
keywords = {intersection types, polymorphism, types, xml},
location = {San Diego, California, USA},
series = {POPL '14}
}

@article{10.1145/2578855.2535840,
author = {Castagna, Giuseppe and Nguyen, Kim and Xu, Zhiwu and Im, Hyeonseung and Lenglet, Sergue\"{\i} and Padovani, Luca},
title = {Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation},
year = {2014},
issue_date = {January 2014},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {49},
number = {1},
issn = {0362-1340},
url = {https://doi.org/10.1145/2578855.2535840},
doi = {10.1145/2578855.2535840},
journal = {SIGPLAN Not.},
month = jan,
pages = {5–17},
numpages = {13},
keywords = {intersection types, polymorphism, types, xml}
}