Post #615304

2026-03-04 08:47 UTC

RE: https://mastoxiv.page/@arXiv_csLO_bot/116169963926058915 Lately I&#39;ve embarked on a fun side quest in proof theory. Where I managed to still bump into bidirectional typing! (To an old dog everything looks like a nail, that&#39;s the saying right?) I learned bidirectionalism is very much related to the subformula property, a proof theory idea that had always seemed mysterious to me. Now I understand why proof theorists rave about cut elimination and the subformula property, which is the same as why bidirectionalism is so useful for proofs: information flow! Also the coincidence between normal forms and terms having good bidirectional typing seems less miraculous: it&#39;s essentially the same thing as cut-free proofs having the subformula property. So anyway, interpolation is a cute property, but I learned a surprising amount about type theory while looking at it! Hope you will too.

Replies (6)

@jonmsterling@mathstodon.xyz 2026-03-04 09:25

@mevenlennonbertrand cool...

Open ##1942211
@consequently@hcommons.social 2026-03-04 09:51

@mevenlennonbertrand This is a really neat paper! I especially appreciated the explanation of the difference between the two different kinds of normal forms in STLC with sums. (And of course, the connections between bidirectional typing and interpolation is natural when you see it.)

Open ##1942212
@ncf@types.pl 2026-03-09 20:28

@mevenlennonbertrand reference 2 has different authors in the text and in the bibliography

Open ##1942213
@ncf@types.pl 2026-03-09 20:45

@mevenlennonbertrand i think i had a similar realisation recently when i saw someone motivate the subformula property by saying "we don't have to guess anything in proof search". it really is not at all about subformulas and all about information flow...

Open ##1942215
@MartinEscardo@mathstodon.xyz 2026-03-09 21:20

@mevenlennonbertrand writes "Lately I've embarked on a fun side quest in proof theory. Where I managed to still bump into bidirectional typing!" Is this yet another instance of "to a man with a hammer, everything looks like a nail?". (It happened to me more than once.)

Open ##1942216
@zanzi@mathstodon.xyz 2026-03-10 10:17

@mevenlennonbertrand very excited to read this!

Open ##1942219