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