Fun

A typed lambda-calculus, similar to SOL[2].

"On Understanding Types, Data Abstractions and Polymorphism", Luca Cardelli et al, ACM Computing Surveys 17(4) (Dec 1985).