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…