O Sistema F com pares possui fortes propriedades de normalização e redução de assunto?

É fácil procurar em muitos livros didáticos as provas de redução de assunto e forte normalização do Sistema F; também, às vezes, existem definições do Sistema F com pares, onde (t, r) é um termo, não apenas uma codificação. A questão é: qual seria a referência para esse sistema?

O tratamento de pares dados por codificação, como o de Provas e Tipos , não é o que você normalmente deseja, pois eles não são "pares de adjetivos", ou seja, não existe uma regra eta. Vamos chamar pares de adjetivos, produtos.

Uma extensão do sistema F com produtos e unidades é apresentada em: Di Cosmo, 1995, isomorfismos dos tipos: do cálculo lambda à recuperação de informações e design de linguagem , Birkhauser: Basel.

Você pode adicionar tipos indutivos arbitrários (positivos) ao sistema F e mostrar que o sistema com eliminadores apropriados é SN. Isso é tratado na tese de Mendler aqui .