Qual é o status atual de programas paralelos ou concorrentes no isomorfismo de Curry-Howard?

Nas provas e tipos de Girard , podemos ler:

Do ponto de vista algorítmico, o cálculo seqüencial não possui isomorfismo de Curry-Howard, devido à multiplicidade de maneiras de escrever a mesma prova. Isso nos impede de usá-lo como um cálcio digitado , embora vislumbremos alguma estrutura profunda desse tipo, provavelmente ligada ao paralelismo.$\lambda$

Provas e tipos , JY Girard (Página 28)

Mas também podemos ler (sobre a Linear Logic) que

Do ponto de vista da ciência da computação, fornece uma nova abordagem para questões de preguiça, efeitos colaterais e alocação de memória [GirLaf, Laf87, Laf88] com aplicações promissoras ao paralelismo.

Provas e tipos , JY Girard (página 149, escrita por Yves Lafont)

Como os programas paralelos estão ligados ao isomorfismo de Curry-Howard? Quais são os pensamentos atuais sobre isso?

O Concurrent Logical Framework é uma área interessante, incluindo seus descendentes, como Linear Meld e LolliMon . Isso é baseado na lógica linear intuicionista.

A lógica linear clássica possui conexões com a CHAM (Linear Chemical Abstract Machine), conforme descrito, por exemplo, em Cálculo para redes de interação com base na Linear Chemical Abstract Machine, que descreve explicitamente o resultado como um resultado do tipo Curry-Howard.

$\lambda\mu$

De qualquer forma, tudo isso ainda é uma área animada de pesquisa. Existem muitos artigos recentes sobre esse assunto. O exposto acima nem sequer menciona o lado ainda mais subestrutural da lógica de separação e a correspondente Teoria de Tipos de Hoare, que se concentra em linguagens de programação imperativas. Por exemplo, há Rumo à semântica teórica do tipo para simultaneidade transacional cujas referências você pode rastrear para trabalhos anteriores.

(Como uma nota pedante, a maioria deles se concentra na concorrência , não no paralelismo em si.)

Para a simultaneidade em geral, há uma linha de pesquisa muito ativa, que tentei resumir nesta resposta: https://cs.stackexchange.com/a/102711/98901

Eu adiciono aqui um comentário sobre paralelismo, abaixo.

Avron [1996] introduziu a noção de hipersquentes , isto é, coleções de sequências em julgamentos.

$\mathcal{G}$$\mathcal{H}$$\mathcal{G} | \mathcal{H}$$|$$P$$Q$$\mathcal G$$\mathcal H$$P|Q$$P$$Q$$\mathcal G | \mathcal H$

Começamos a arranhar a superfície da interpretação semântica disso, mas o paralelismo é bastante evidente: a semântica da composição paralela permite ver ações simultâneas de ambos os processos, e há um teorema no artigo que afirma que nenhum dos dois os dois processos precisam esperar que o outro execute pelo menos alguma ação (o Teorema da Prontidão). A extensão para mais de duas ações ao mesmo tempo parece direta. (A digitação já permite isso, mas a semântica nesse artigo não tira proveito disso.)