Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Wed 21 Sep 2016 11:25 - 11:50 at Noh Theater - Session 9 Chair(s): Sam Lindley

Dunfield showed that a simply typed core calculus with intersection
types and a merge operator is able to capture various programming
language features. While his calculus is type-safe, it is not
coherent: different derivations for the same expression can
elaborate to expressions that evaluate to different values.
The lack of coherence is an important
disadvantage for adoption of his core calculus in implementations of
programming languages, as the semantics of the programming language
becomes implementation-dependent.

This paper presents λi: a coherent and type-safe calculus with a
form of *intersection types and a merge operator.
Coherence is achieved by ensuring that intersection types
are disjoint and programs are sufficiently
annotated to avoid type ambiguity. We propose a definition of disjointness where two
types A and B are disjoint only if certain set of types are common
supertypes of A and B. We investigate three different variants of
λi, with three variants of disjointness. In the simplest
variant, which does not allow top types, two types are disjoint if
they do not share any common supertypes at all. The other two variants
introduce top types and refine the notion of disjointness to allow
two types to be disjoint when the only the set of common supertypes are
top-like. The difference between the two variants with top
types is on the definition of top-like types, which has an impact on
which types are allowed on intersections. We present a type system
that prevents intersection types that are not disjoint, as well as an
algorithmic specifications to determine whether two types are disjoint
for all three variants.

Wed 21 Sep (GMT+09:00) Osaka, Sapporo, Tokyo change

10:35 - 12:15: Research Papers - Session 9 at Noh Theater
Chair(s): Sam LindleyUniversity of Edinburgh, UK
icfp-2016-papers10:35 - 11:00
Trevor L. McDonellIndiana University, USA, Timothy A. K. ZakianOxford University, UK, Matteo CiminiIndiana University, USA, Ryan R. NewtonIndiana University, USA
icfp-2016-papers11:00 - 11:25
David ThibodeauMcGill University, Canada, Andrew CaveMcGill University, Canada, Brigitte PientkaMcGill University, Canada
icfp-2016-papers11:25 - 11:50
Bruno C. d. S. OliveiraUniversity of Hong Kong, China, Zhiyuan ShiUniversity of Hong Kong, China, João AlpuimUniversity of Hong Kong, China
icfp-2016-papers11:50 - 12:15
Giuseppe CastagnaParis Diderot University & CNRS, Tommaso PetruccianiUniversity of Genoa, France, Kim NguyễnUniversity of Paris-Sud, France