[Prev][Next][Index][Thread]

Origin of type-labeled lambda abstraction



Date: Thu, 6 Feb 92 17:02:05 EST

Who introduced type-labeled lambda abstraction, i.e., the version of the
lambda-operator that leads to terms of the form lambda x : sigma . Z, where
sigma is a type symbol?  I have the impression that this version of
abstraction comes from AUTOMATH, but I'm not sure, and, even if that's
right, I don't know which of the AUTOMATH people came up with it.

Garrel Pottinger
garrel@oracorp.com