Post #1942216
2026-03-09 21:20 UTC
@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.)
Replies (1)
-
@mevenlennonbertrand@lipn.info 2026-03-09 22:19
@MartinEscardo That's just what I (jokingly) meant in the next sentence ;) So yes to some extent it is, since this is very much me trying to make sense of proof theory I am re-casting it with my own words. But somehow what I wanted to put forward is that it brought a new (to me) light on something (bidirectional typing) I already understood, by looking at it in a different context. It's probably a bit pretentious a claim at this stage, but I feel this is a tentative new entry in the Curry-Howard correspondence, which, as we know, is a nice way to understand things we think we know.