## Stream: Type theory

### Topic: Classical logic

#### Brandon Brown (May 13 2020 at 06:55):

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 (May 13 2020 at 07:08):

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

#### Kevin Buzzard (May 13 2020 at 07:23):

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

#### Patrick Stevens (May 13 2020 at 07:45):

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 (May 13 2020 at 07:56):

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 (May 13 2020 at 07:57):

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 (May 13 2020 at 08:05):

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.

Last updated: May 08 2021 at 21:09 UTC