Talk at Deducteam seminar: The exp-log normal form of types and canonical forms of terms
In presence of sum types, the lambda calculus does not enjoy uniqueness of eta-long normal forms. The canonicity problem also appears for proof trees of intuitionistic logic. In this talk, I will show how the problem becomes easier if, before choosing a canonical representative from a class of beta-eta-equal terms, one coerces the term into the exp-log normal form of its type. This type normal form arises from the one for exponential polynomials.
Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net