Re: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)

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? :)

>