Non determinism through type isomorphism

(English below)

Con Gilles Dowek hemos enviado un nuevo artículo para revisión. Una versión muy preliminar de este artículo es lo que presentamos en la semana Enfoques Cuantitativos del LI2012.

Aquí dejo una traducción del título y resumen:

No determinismo por medio de isomorfismo de tipos 

Definimos una relación de equivalencia sobre proposiciones y un sistema de pruebas donde proposiciones equivalentes tienen la misma prueba. El sistema obtenido es similar a varios lambda-cálculo no determinísticos y algebraicos. Este sistema tiene preservación de tipos y normalización fuerte.

En las conclusiones del artículo se pueden ver varios problemas para trabajos futuros, y la posible conexión con los lenguajes cuánticos.

Actualización: El paper ha sido aceptado en LSFA 2012. La versión corregida se encuentra disponible en mi página web (próximamente en EPTCS) en EPTCS 113:137-144, 2013.

---

Gilles Dowek and I have just sent a paper for review. A very preliminary version of this paper is what we presented in the Quantitative Approaches week of LI2012.

Here is the abstract:

Non determinism through type isomorphism 

We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi. This system enjoys subject reduction and strong normalisation.

Update: The paper has been accepted in LSFA 2012. The corrected version is available for download from my web page. (soon at EPTCS) EPTCS 113:137-144, 2013.