The Coq mailing list

[Danko Ilik <dankoilik AT gmail.com>]

Hi Jason,

You can also probably find some more references of relevance in my POPL 2017 paper on the subject, available here: https://arxiv.org/pdf/1502.04634

Best regards,

Danko

On Tue, Mar 30, 2021 at 5:16 AM roux cody <cody.roux AT gmail.com> wrote:

I've always enjoyed "On the Strong Normalisation of NaturalDeduction with Permutation-Conversions" By P. de Groote. It proves normalization directly, not NbE, though, and uses a CPS translation to turn the problem with sums into STLC with only negative types.

It's probably worth spending some time understanding the paper you cited though, in my humble opinion.

Best,

Cody

On Mon, Mar 29, 2021 at 10:38 PM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

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/