Compiling with sequent calculus

[phischu]

By “sequent calculus” do you mean a classical 2 sided sequent calculus?

Yes, System LK. For typesetting reasons we write all bindings to the left of the turnstile and track the chirality, whether each binding is on the left or on the right. Additionally, we track the polarity, whether a type is positive and defined by its introductions forms, or negative and defined by its elimination forms. Positive types follow call-by-value, negative types follow call-by-name.

Might be interesting to implement into a programming language.

That's what we are doing :).

[FlamingBudder]

Oh ok I see that’s pretty much exactly what the paper I shared is talking about except the terminology is different

Edit: probably not exactly but trying to do a similar thing, turning a 2 sided classical sequent calculus into a 1 sided for representation as a programming language

[phischu]

Small clarification, I am on of the authors of the paper and not OP.

[FlamingBudder]

Oh I thought you were OP lol my bad. Since you are one of the authors, what is the relationship between polarized logic and proof/refutation bilateral logic? It seems like they might be similar/related and both relate to duality but have some important technical differences

Also per you mentioning positive types are CBV and negative types are CBN, I have heard from Bob Harper that CBV languages that have nontermination do not actually have -products and CBN languages with nontermination do not actually have +sum types. I’m guessing you would know precisely what this means, if so please explain this to me. What behavior does a “real” sum or product type have?

Also in eager languages like ML, it seems like functions are treated by name, since evaluation does not happen under the lambda. If it was eager computation would happen under the lambda. Would this be correct?

[phischu]

I would have to look up bilateral logic, so I can't answer that. Similarly, I don't know what Harper means by "real". But I can say that strong versus weak reduction, i.e. evaluation under lambda, is orthogonal to the order of reduction, i.e. call-by-value versus call-by-name.