Ciência da Computação Teórica polymorphism
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?