Polymorphic System I

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.

arXiv comment20 pages plus appendix

References in corpus (7)

• Dynamic Choreographies: Theory And Implementation
• Lineal: A linear-algebraic Lambda-calculus
• The Vectorial $\lambda$-Calculus
• Pure Type Systems without Explicit Contexts
• Non determinism through type isomorphism
• Polymorphic System I
• Extensional proofs in a propositional logic modulo isomorphisms

Cited by in corpus (2)

• Polymorphic System I
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus