2 papers
cs.LO2026
Principal Typing for Intersection Types, Forty-Five Years Later
Daniele Pautasso, Simona Ronchi Della Rocca
A type assignment system for lambda-calculus enjoys the principal typing property if every typable term M has a special typing, called principal, from which all typings for M can b…
cs.LO2026
Strong normalization through idempotent intersection types: a new syntactical approach
Pablo Barenbaum, Simona Ronchi Della Rocca, Cristian Sottile
It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems r…