Polymorphic System I
Cristian F. Sottile, Alejandro D\'iaz-Caro, and Pablo E. Mart\'inez, L\'opez
TL;DR
This paper extends System I, a simply-typed lambda calculus with pairs, to polymorphic types, incorporating type isomorphisms and providing proofs of key properties like subject reduction and strong normalization.
Contribution
It introduces a polymorphic extension of System I with type isomorphisms and offers non-standard proofs of fundamental properties.
Findings
Extended System I to polymorphic types with isomorphisms
Proved subject reduction for the extended system
Established strong normalization through novel proofs
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.