ICC 25427
INSTITUTO DE INVESTIGACION EN CIENCIAS DE LA COMPUTACION
Unidad Ejecutora - UE
artículos
Título:
Polymorphic System I
Autor/es:
CRISTIAN F. SOTTILE; PABLO E. MARTÍNEZ LÓPEZ; ALEJANDRO DÍAZ-CARO
Revista:
ACM International Conference Proceeding Series
Editorial:
Association for Computing Machinery
Referencias:
Año: 2020 vol. IFL p. 127 - 137
ISSN:
2590-1184
Resumen:
System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an extension of System I to polymorphic types, adding the corresponding isomorphisms. We provide non-standard proofs of subject reduction and strong normalisation, extending those of System I.
