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

esop-2019-papers
10:30 - 12:30: ESOP 2019 - Types at SUN II
Chair(s): Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon
esop-2019-papers10:30 - 11:00
Talk
Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Link to publication
esop-2019-papers11:00 - 11:30
Talk
Xuan BiStandard Chartered Bank, Ningning XieThe University of Hong Kong, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong, Tom SchrijversKU Leuven
Link to publication
esop-2019-papers11:30 - 12:00
Talk
Beniamino AccattoliInria & Ecole Polytechnique, Giulio GuerrieriUniversity of Bath, Maico Leberle
Link to publication
esop-2019-papers12:00 - 12:30
Talk
Link to publication