Path: ...!2.eu.feeder.erje.net!3.eu.feeder.erje.net!feeder.erje.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: How to make cyclic terms (Was: A miraculous match?)
Date: Thu, 9 Jan 2025 17:14:15 +0100
Message-ID: <vloskn$2djmt$1@solani.org>
References: <vlkfq7$1vh4j$1@solani.org> <vlkrge$2dkpc$1@dont-email.me>
 <vllgli$2039r$1@solani.org> <vlmdk8$2dkpd$6@dont-email.me>
 <vlme6h$2dkpc$3@dont-email.me> <vlo9os$2dkpd$11@dont-email.me>
 <vloa2b$2dkpd$12@dont-email.me> <vlof4t$21qd0$1@solani.org>
 <vlok49$2dkpc$8@dont-email.me> <vlorvp$2dj8n$1@solani.org>
 <vlos4h$2dj8n$2@solani.org> <vlos83$2dj8n$4@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 9 Jan 2025 16:14:15 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2543325"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101
 Firefox/128.0 SeaMonkey/2.53.20
Cancel-Lock: sha1:HFWpCwOR8bVV0MCpIVaA6KPesxs=
X-User-ID: eJwFwYkBwCAIBLCVpNxTxxEs+4/QhKlQG6LA4fh6ePbDjs+jxZq4tFoDpQAtx7Na6PN+u8qDyuTBTVf0D0fAFTk=
In-Reply-To: <vlos83$2dj8n$4@solani.org>
Bytes: 2000
Lines: 26

Also Hiroshi Nakano paper is not
about System F, since the type binder

is not motivated by let polymorphism of
Hindley-Milner but rather by least fixpoint

theories, trying to capture recursive types.

Mild Shock schrieb:
> Corr.: System T ~~> System F
> 
> Mild Shock schrieb:
>> Hi,
>>
>> I told you a dozen times that the scope of
>> this thread is simple types. Why don't you
>> open a separate thread for your fetish
>>
>> System T and/or Coq. I really don't care
>> about System T. You can play online with
>> System T here:
>>
>> https://crypto.stanford.edu/~blynn/lambda/systemf.html
>>
>> Bye
>