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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10
|Deciding equivalence with sums and the empty type
Gabriel Scherer Northeastern University
|The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
Danko Ilik Trusted Labs
|Typed Self-Evaluation via Intensional Type Functions