<p>It is commonsense that STLC corresponds to Gentzen's natural deduction proof system, where the elimination of implication is defined in terms of modus ponens. Sequent calculus, however, is more of a &quot;continuation&quot;-based style, but some other connectives (like the different choices in linear sequent calculus) look more interesting than just CPS-ed STLC.</p>
<p>So I wonder, what is the canonical PL that CH-corresponds to sequent calculus?</p>

<lambda-calculus>
What kind programming language corresponds to sequent calculus?
CC BY-SA 4.0
2024-02-19T18:12:31.100Z
Wouldn't that question be more at home on cs.stackexchange.com?
Eldritch Conundrum
CC BY-SA 4.0
2024-02-20T04:06:08.667Z
@EldritchConundrum I have the impression that no PL people actually checks that website. For this one, there are slightly more. Proof Assistants is active, but this question might be too easy for that site
ice1000
CC BY-SA 4.0
2024-02-20T20:52:05.823Z
This isn't an _answer_ to your question - thus a comment - but the Shen language implements static type checking via the sequent calculus.
davidbak
CC BY-SA 4.0
2024-03-09T21:17:06.923Z
@ice1000: We do check that web site.
Andrej Bauer
<p>I don't think there's any &quot;canonical PL&quot; for sequent calculus, because languages based on it are rare, and none are well-known.</p>
<p><a href="https://dl.acm.org/doi/10.1145/3022670.2951931" rel="noreferrer">Sequent Calculus as a Compiler Intermediate Language</a> is an experiment using an intermediate language based on sequent calculus in GHC, which is most likely the closest sequent calculus has come to touching production code. It is an intuitionistic calculus, so unlike classical calculi, there can only be one variable in the right context.</p>
<p>More academically, I found <a href="https://doi.org/10.4230/LIPIcs.TLCA.2015.165" rel="noreferrer">Curry-Howard for Sequent Calculus at Last!</a> a useful reference for understanding how to compute with classical sequent calculi. I don't know how it compares to the papers rpjohnst linked, which I have not read.</p>
<p>As rpjohnst mentioned, it's generally possible to translate between natural deduction and sequent calculi, so it's not a whole new paradigm in the same way that logic programming or imperative programming are (relative to functional programming).</p>
<p>However, that doesn't mean that sequent calculus is without merit. It's more explicit with control flow, giving it some similar advantages to CPS (as described in <a href="https://dl.acm.org/doi/10.1145/3022670.2951931" rel="noreferrer">Sequent Calculus as a Compiler Intermediate Language</a>).</p>
<p>Additionally, its symmetry makes adds clarity when working with <a href="https://ncatlab.org/nlab/show/polarity+in+type+theory" rel="noreferrer">dual types</a>, so it might be a more suitable framework for exploring programming languages which distinguish data and codata (which effectful languages ought to) or languages based on classical logic or paraconsistent logics. (Compare and contrast <a href="https://www.cs.bham.ac.uk/%7Epbl/papers/tlca99.pdf" rel="noreferrer">call-by-push-value</a>.) <a href="https://www.elegantobjects.org/" rel="noreferrer">Elegant Objects</a> looks more-or-less just like programming with codata to me, so sequent calculus might also be a good framework for someone who likes theory and wants to make a multi-paradigm functional/OO language.</p>
<p>Even for intuitionistic languages, I find the symmetry worthwhile for its own sake, because it pleases me. If you're interested in sequent calculus for its symmetry, I found <a href="https://www.math.unipd.it/%7Esambin/txt/SBF.pdf" rel="noreferrer">Basic logic: reflection, symmetry, visibility</a> helpful because it gives an idea of some of the principles which you might want to follow when translating your own inference rules into sequent calculus. It's also interesting to contrast against comparable computer science papers if you want to learn the Curry-Howard (literal) translation between type theory and formal logic terms. (It also describes the dual to implication and dual intuitionistic logic, if you're into that sort of thing.)</p>

CC BY-SA 4.0
2024-02-20T04:09:31.247Z
2024-02-20T04:09:31.247Z
James Martin
<p>There are languages like the μ̃μ calculus, as described by e.g. this tutorial (particularly section 4 onward): <a href="https://ix.cs.uoregon.edu/%7Epdownen/publications/sequent-intro.pdf" rel="noreferrer">https://ix.cs.uoregon.edu/~pdownen/publications/sequent-intro.pdf</a></p>
<p>Lambda calculus terms produce values which are consumed by their context, corresponding to natural deduction introduction (e.g. <code>λx.e</code> producing a function) and elimination (e.g. <code>f a</code> consuming the function and producing its result).</p>
<p>Terms in the μ̃μ calculus are split into producers, consumers, and commands. Producer terms come from right rules, consumer terms come from left rules, and commands come from the cut rule. So for example, a command term that cuts a function producer with a function consumer looks like <code>⟨λx.e||a.α⟩</code>, where the consumer variable <code>α</code> receives <code>e[a/x]</code>.</p>
<p>The μ̃μ calculus gets its name from μ terms that let a producer or consumer name its output or input, respectively. A μ producer term looks a lot like a control operator (e.g. call/cc), as it binds a continuation variable for use in an inner command: in <code>⟨μα.⟨e||β⟩||...⟩</code>, <code>α</code> refers to the <code>...</code>. The dual consumer term lets a consumer bind its input value.</p>
<p>Each additional connective in this system gets producer and consumer terms, and gets a β reduction to define how they interact in a command. For example, pairs would have producer terms like <code>(a, b)</code>, and consumer terms like <code>fst . α</code> and <code>snd . α</code>. As more exotic example, a <code>⅋</code> producer term might look like <code>[α,β].⟨...||...⟩</code> (bind two continuations in a command), while its consumer would look like <code>(α,β)</code> (a pair of continuations to be bound).</p>
<p>It's generally possible to translate between lambda calculus/natural deduction and μ̃μ/sequent calculus in a mechanical way. This paper describes a language with both introduction/elimination and left/right rules, and shows how these languages are related: <a href="https://ps.informatik.uni-tuebingen.de/publications/ostermann22introelim.pdf" rel="noreferrer">https://ps.informatik.uni-tuebingen.de/publications/ostermann22introelim.pdf</a></p>

CC BY-SA 4.0
2024-02-19T23:49:36.177Z
2024-02-19T23:49:36.177Z
rpjohnst
CC BY-SA 4.0
2024-02-20T03:42:21.523Z
Thanks very much!
ice1000
# What kind programming language corresponds to sequent calculus?
Posted by: username_0 on 2024-02-19
It is commonsense that STLC corresponds to Gentzen's natural deduction proof system, where the elimination of implication is defined in terms of modus ponens. Sequent calculus, however, is more of a "continuation"-based style, but some other connectives (like the different choices in linear sequent calculus) look more interesting than just CPS-ed STLC.

So I wonder, what is the canonical PL that CH-corresponds to sequent calculus?
**Tags:** lambda-calculus
> **Comments:**
> **username_1**: Wouldn't that question be more at home on cs.stackexchange.com?  
> **username_0**: @EldritchConundrum I have the impression that no PL people actually checks that website. For this one, there are slightly more. Proof Assistants is active, but this question might be too easy for that site  
> **username_2**: This isn't an _answer_ to your question - thus a comment - but the Shen language implements static type checking via the sequent calculus.  
> **username_3**: @ice1000: We do check that web site.  
---
## 2 answers
### Answer by username_5 on 2024-02-19. Score: 8 | Accepted answer
There are languages like the μ̃μ calculus, as described by e.g. this tutorial (particularly section 4 onward): [https://ix.cs.uoregon.edu/~pdownen/publications/sequent-intro.pdf](https://ix.cs.uoregon.edu/%7Epdownen/publications/sequent-intro.pdf)

Lambda calculus terms produce values which are consumed by their context, corresponding to natural deduction introduction (e.g. `λx.e` producing a function) and elimination (e.g. `f a` consuming the function and producing its result).

Terms in the μ̃μ calculus are split into producers, consumers, and commands. Producer terms come from right rules, consumer terms come from left rules, and commands come from the cut rule. So for example, a command term that cuts a function producer with a function consumer looks like `⟨λx.e||a.α⟩`, where the consumer variable `α` receives `e[a/x]`.

The μ̃μ calculus gets its name from μ terms that let a producer or consumer name its output or input, respectively. A μ producer term looks a lot like a control operator (e.g. call/cc), as it binds a continuation variable for use in an inner command: in `⟨μα.⟨e||β⟩||...⟩`, `α` refers to the `...`. The dual consumer term lets a consumer bind its input value.

Each additional connective in this system gets producer and consumer terms, and gets a β reduction to define how they interact in a command. For example, pairs would have producer terms like `(a, b)`, and consumer terms like `fst . α` and `snd . α`. As more exotic example, a `⅋` producer term might look like `[α,β].⟨...||...⟩` (bind two continuations in a command), while its consumer would look like `(α,β)` (a pair of continuations to be bound).

It's generally possible to translate between lambda calculus/natural deduction and μ̃μ/sequent calculus in a mechanical way. This paper describes a language with both introduction/elimination and left/right rules, and shows how these languages are related: <https://ps.informatik.uni-tuebingen.de/publications/ostermann22introelim.pdf>
> **Comments:**
> **username_0** (2024-02-20): Thanks very much!  
---
### Answer by username_4 on 2024-02-20. Score: 8
I don't think there's any "canonical PL" for sequent calculus, because languages based on it are rare, and none are well-known.

[Sequent Calculus as a Compiler Intermediate Language](https://dl.acm.org/doi/10.1145/3022670.2951931) is an experiment using an intermediate language based on sequent calculus in GHC, which is most likely the closest sequent calculus has come to touching production code. It is an intuitionistic calculus, so unlike classical calculi, there can only be one variable in the right context.

More academically, I found [Curry-Howard for Sequent Calculus at Last!](https://doi.org/10.4230/LIPIcs.TLCA.2015.165) a useful reference for understanding how to compute with classical sequent calculi. I don't know how it compares to the papers rpjohnst linked, which I have not read.

As rpjohnst mentioned, it's generally possible to translate between natural deduction and sequent calculi, so it's not a whole new paradigm in the same way that logic programming or imperative programming are (relative to functional programming).

However, that doesn't mean that sequent calculus is without merit. It's more explicit with control flow, giving it some similar advantages to CPS (as described in [Sequent Calculus as a Compiler Intermediate Language](https://dl.acm.org/doi/10.1145/3022670.2951931)).

Additionally, its symmetry makes adds clarity when working with [dual types](https://ncatlab.org/nlab/show/polarity+in+type+theory), so it might be a more suitable framework for exploring programming languages which distinguish data and codata (which effectful languages ought to) or languages based on classical logic or paraconsistent logics. (Compare and contrast [call-by-push-value](https://www.cs.bham.ac.uk/%7Epbl/papers/tlca99.pdf).) [Elegant Objects](https://www.elegantobjects.org/) looks more-or-less just like programming with codata to me, so sequent calculus might also be a good framework for someone who likes theory and wants to make a multi-paradigm functional/OO language.

Even for intuitionistic languages, I find the symmetry worthwhile for its own sake, because it pleases me. If you're interested in sequent calculus for its symmetry, I found [Basic logic: reflection, symmetry, visibility](https://www.math.unipd.it/%7Esambin/txt/SBF.pdf) helpful because it gives an idea of some of the principles which you might want to follow when translating your own inference rules into sequent calculus. It's also interesting to contrast against comparable computer science papers if you want to learn the Curry-Howard (literal) translation between type theory and formal logic terms. (It also describes the dual to implication and dual intuitionistic logic, if you're into that sort of thing.)
---
