Classical logic

Stream: Type theory

[Brandon Brown]

Just found this paper "Classical Proofs as Parallel Programs" wherein they devise a typed lambda calculus with concurrency and show it models classical logic. < https://arxiv.org/pdf/1809.03094.pdf >

[Kenny Lau]

Actually I've never understood what call/cc does or why it corresponds to ((A -> B) -> A) -> A

[Kevin Buzzard]

This was the point where I stopped following Leroy's College de France lectures

[Patrick Stevens]

Kenny Lau said:

Actually I've never understood what call/cc does or why it corresponds to ((A -> B) -> A) -> A

I'm in the middle of writing a big blurb about this, actually - call/cc is one of those things that's really simple once you've spent many hours thinking about it, but sadly I don't think there's a magic analogy that makes it obvious

[Anne Baanen]

Here's my path to enlightenment. I was meditating on return-from, unwind-protect, throw and catch, when I realized this (almost!) works:

(defun call/cc (body)
        (apply body (lambda (x) (return-from call/cc x)) nil))

[Anne Baanen]

return-from call/cc x is like return x but returns from the call to call/cc that constructed the lambda, instead of the lambda itself.

[Brandon Brown]

The paper I posted proposes a typed lambda calculus that does not seem to rely on the call/cc operator for its model of classical logic.