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 (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|10:30 - 10:55|
Gabriel SchererNortheastern University
|10:55 - 11:20|
Danko IlikTrusted Labs
|11:20 - 11:45|
|11:45 - 12:10|