Tipos de sessão sem contexto polimórficos de ordem superior

Apresentamos uma extensão dos tipos de sessão sem contexto polimórficos que permite a passagem de canais sobre canais, comumente conhecidos como tipos de sessão de ordem superior. A mistura de tipos funcionais e tipos de sessão provou ser um desafio para a formulação da equivalência de tipos: enquanto a equivalência de tipos funcionais é muitas vezes indutiva e apresentada como um sistema de regras de derivação, a equivalência de tipos de sessão é frequentemente coindutiva e geralmente apresentada como uma bisimulação. Propomos uma abordagem unificadora que lida com a equivalência de tipos funcionais e tipos de sessão sem contexto de ordem superior juntos na forma de um sistema de regras gerando uma relação definida coindutivamente. A decidibilidade da equivalência de tipos é obtida por meio da redução à bisimulação para gramáticas simples, para as quais algoritmos práticos são conhecidos. Para preencher a lacuna entre tipos e gramáticas simples, introduzimos uma linguagem de tipos com nomes canônicos em vez de ligações (que chamamos de c-types) e propomos uma noção de renomeação canônica para traduzir tipos em c-types.