Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation

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).