En las Pruebas y Tipos de Girard podemos leer:
Desde un punto de vista algorítmico, el cálculo posterior no tiene isomorfismo de Curry-Howard, debido a la multitud de formas de escribir la misma prueba. Esto nos impide usarlo como un cálculo tipificado, aunque vislumbramos alguna estructura profunda de este tipo, probablemente vinculada con el paralelismo.
Pruebas y Tipos , JY Girard (Página 28)
Pero también podemos leer (sobre Linear Logic) que
Desde el punto de vista de la informática, ofrece un nuevo enfoque a las cuestiones de pereza, efectos secundarios y asignación de memoria [GirLaf, Laf87, Laf88] con aplicaciones prometedoras para el paralelismo.
Pruebas y tipos , JY Girard (Página 149, escrito por Yves Lafont)
¿Cómo se vinculan los programas paralelos con el isomorfismo de Curry-Howard? ¿Cuáles son los pensamientos actuales sobre eso?
par
para controlarlo (es decir , se podría usar un orden de reducción menos paralelo por defecto que podría hacerse selectivamente más paralelo) pero no tendrían un significado lógico.Para la concurrencia en general, hay una línea de investigación muy activa, que intenté resumir en esta respuesta: https://cs.stackexchange.com/a/102711/98901
Agrego aquí un comentario sobre paralelismo, a continuación.
Avron [1996] introdujo la noción de hipersecuentes , es decir, colecciones de secuencias en juicios.
Acabamos de empezar a rascar la superficie de la interpretación semántica de esto, pero es evidente que esto es paralelismo: la semántica de la composición paralela permite ver acciones simultáneas de ambos procesos, y hay un teorema en el documento que establece que ninguno de los dos los dos procesos deben esperar a que el otro realice al menos alguna acción (el Teorema de preparación). La extensión a más de dos acciones al mismo tiempo parece sencilla. (La escritura ya lo permite, pero la semántica en ese documento no lo aprovecha por completo).
fuente