Agregando polimorfismo a una lógica que identifica proposiciones isomorfas
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...
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Español |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/141023 http://50jaiio.sadio.org.ar/pdfs/est/EST-09.pdf |
| Aporte de: |
| Sumario: | 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. |
|---|