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

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