ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 11:00 - 11:30 at SUN II - Types Chair(s): Vasco T. Vasconcelos

Popular programming techniques such as shallow embeddings of Domain Specific Languages (DSLs), finally tagless or object algebras are built on the principle of compositionality. However, existing programming languages only support simple compositional designs well, and have limited support for more sophisticated ones. This paper presents the F+i calculus, which supports highly modular and compositional designs that improve on existing techniques. These improvements are due to the combination of three features: disjoint intersection types with a merge operator; parametric (disjoint) polymorphism; and BCD-style distributive subtyping. The main technical challenge is F+i’s proof of coherence. A naive adaptation of ideas used in System F’s parametricity to canonicity (the logical relation used by F+i to prove coherence) results in an ill-founded logical relation. To solve the problem our canonicity relation employs a different technique based on immediate substitutions and a restriction to predicative instantiations. Besides coherence, we show several other important meta-theoretical results, such as type-safety, sound and complete algorithmic subtyping, and decidability of the type system. Remarkably, unlike F<:’s bounded polymorphism, disjoint polymorphism in F+i supports decidable type-checking.

Tue 9 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
TypesESOP at SUN II
Chair(s): Vasco T. Vasconcelos University of Lisbon, Portugal
10:30
30m
Talk
Handling polymorphic algebraic effects
ESOP
Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Link to publication
11:00
30m
Talk
Distributive Disjoint Polymorphism for Compositional Programming
ESOP
Xuan Bi Standard Chartered Bank, Ningning Xie University of Toronto, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong, Tom Schrijvers KU Leuven
Link to publication
11:30
30m
Talk
Types by Need
ESOP
Beniamino Accattoli Inria & Ecole Polytechnique, Giulio Guerrieri University of Bath, Maico Leberle
Link to publication
12:00
30m
Talk
Verifiable certificates for predicate subtyping
ESOP
Link to publication