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

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

10:30 - 12:10
Type Systems 2POPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
10:30
25m
Talk
Deciding equivalence with sums and the empty type
POPL
Gabriel Scherer Northeastern University
10:55
25m
Talk
The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
POPL
Danko Ilik Trusted Labs
11:20
25m
Talk
Contextual isomorphisms
POPL
11:45
25m
Talk
Typed Self-Evaluation via Intensional Type Functions
POPL
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles