[TYPES] normalization by evaluation for strong sums for STLC

[Jason -Zhong Sheng- Hu]

Hi all,

I am trying to find papers on NbE algorithms handling strong sums for STLC. In particular, I want to see how this commuting conversion rule is dealt with:

(match t with
| inl y => s
| inr z => u) t'
============>
match t with
| inl y => s t'
| inr z => u t'

that is, applications immediately after a pattern matching are distributed into the branches.

For most papers I found, they only deal with either other commuting conversions or eta for sums. I am aware of https://ieeexplore.ieee.org/document/932506 which does handle that commuting conversion in interest, but it is too category-heavy. I am looking for more light-weight semantic methods. Is there any other method to deal with strong sums which I am not aware of?

Thanks,
Jason Hu
https://hustmphrrr.github.io/