[TYPES] (no subject)

[Jonathan Seldin]

It is in Curry's theory of functionality, which is presented in  
chapters 9 and 10 of Combinatory Logic, volume I, and it is also  
discussed in Combinatory Logic, volume II (North-Holland, Amsterdam,  
1972), Chapter 14.  There are references to earlier works on the  
theory in volume I.

On 17-Mar-09, at 8:35 AM, Beta Ziliani wrote:


> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> The second approach is based on the work of Curry in Combinatory  
> Logic. I
> think it's in
> Curry [1958]: Combinatory Logic Vol. I (North-Holland, Amstedam)
> but I'm not completely sure.
>
> Best,
> Beta
>
> On Tue, Mar 17, 2009 at 9:28 AM, Andrew Pitts  
> <Andrew.Pitts at cl.cam.ac.uk>wrote:
>
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>> types-list]
>>
>> When formulating a type theory there are (at least) two different
>> approaches to how variables are typed:
>>
>> - variables come tagged with an explicit type
>>
>> - variables are assigned types in a typing context that forms part of
>> the typing judgement
>>
>> I believe that the first approach can be traced back to Church's
>> original 1940 paper on the Simple Theory of Types. Can any one  
>> tell me
>> about the origins of the second approach?
>>
>> Andy Pitts
>>

Jonathan P. Seldin                                     tel: 403-329-2364
Department of Mathematics and Computer Science  jonathan.seldin at uleth.ca
University of Lethbridge                              seldin at cs.uleth.ca
4401 University Drive                    http://www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4