[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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/
