Path: ...!news.nobody.at!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: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)
Date: Tue, 17 Dec 2024 21:01:19 +0100
Message-ID: <vjslaf$1dmbi$2@solani.org>
References: <vjks2t$sghb$1@solani.org> <vjksaq$sgo6$1@solani.org>
 <vjksdb$sgo6$2@solani.org> <vjs63g$1m603$1@dont-email.me>
 <vjsl6t$1dmbi$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 17 Dec 2024 20:01:19 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1497458"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:2vyMazg0ionnwYIyOsE6vVcCWoE=
X-User-ID: eJwNxsEBwCAIA8CVFBKg41gw+4/Q3uvosaMTwQBF7Shfg9P/xvqRGTl5s2y66+Ta5bodL92OTAg5Kke6SOADU0YVpA==
In-Reply-To: <vjsl6t$1dmbi$1@solani.org>
Bytes: 1955
Lines: 34

Hi,

Some other ones are here:

Linear Logic and Lazy Computation
J. Y. Girard and Y. Lafont - TAPSOFT '87
https://www.researchgate.net/publication/226363607

But they have also other connectives, not only implication.

Bye

Mild Shock schrieb:
> Hi,
> 
> For a combinatory logic there is a hint here:
> 
> 5. Linear (BCI) and affine (BCK) combinatory logic
> https://ncatlab.org/nlab/show/combinatory+logic#LinearAndAffine
> 
> But I guess there are other ones as well?
> 
> Bye
> 
> P.S.: I didn't verfy whether BCK and BCI are really
> affine and linear. They write combinator I is also
> definable as CKK, this would give an embedding of affine
> 
> into linear. But possibly not vice versa? Can we show
> all these things via Prolog?
> 
> Julio Di Egidio schrieb:
>> Sounds good?  Anything else? :)
>