POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 10:30 - 10:55 at Auditorium - Type Systems 2 Chair(s): Andrew D. Gordon

The logical technique of focusing can be applied to the λ-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with βη-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types and the empty type). This rich structure let us prove the decidability of βη-equivalence in presence of the empty type, the fact that it coincides with contextual equivalence, and with set-theoretic equality in all finite models.

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: Type Systems 2POPL at Auditorium
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh
10:30 - 10:55
Talk
POPL
Gabriel SchererNortheastern University
10:55 - 11:20
Talk
POPL
Danko IlikTrusted Labs
11:20 - 11:45
Talk
POPL
11:45 - 12:10
Talk
POPL
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles