Agregando polimorfismo a una lógica que identifica proposiciones isomorfas

Abstract

Sistema I es un cálculo lambda simplemente tipado con pares, extendido con una teoría ecuacional obtenida a partir de considerar a los tipos isomorfos como iguales. En este trabajo presentamos una extensión de Sistema I a polimorfismo, agregando los isomorfismos correspondientes, y proveemos pruebas no estándar de las propiedades de preservación de tipos y normalización fuerte.