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

A cornerstone of the theory of lambda-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho’s system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.

Tue 9 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30: TypesESOP at SUN II
Chair(s): Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon
10:30 - 11:00
Talk
Handling polymorphic algebraic effects
ESOP
Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Link to publication
11:00 - 11:30
Talk
Distributive Disjoint Polymorphism for Compositional Programming
ESOP
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
11:30 - 12:00
Talk
Types by Need
ESOP
Beniamino AccattoliInria & Ecole Polytechnique, Giulio GuerrieriUniversity of Bath, Maico Leberle
Link to publication
12:00 - 12:30
Talk
Verifiable certificates for predicate subtyping
ESOP
Link to publication