{"ID":2831680,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2512.07511","arxiv_id":"2512.07511","title":"Canonical bidirectional typechecking","abstract":"We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised $μ\\tildeμ$-calculus. Specifically, positive terms and negative coterms are checkable, and negative terms and positive coterms are synthesisable. This combines a standard formulation of bidirectional typechecking with Zeilberger's `cocontextual' variant. We extend this to ordinary `cartesian' System L using Mc Bride's co-de Bruijn formulation of scopes, and show that both can be combined in a linear-nonlinear style, where linear types are positive and cartesian types are negative. This yields a remarkable 3-way coincidence between the shifts of polarised System L, LNL calculi, and bidirectional calculi.","short_abstract":"We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised $μ\\tildeμ$-calculus. Specifically, positive terms and negative coterms are checkable, and negative terms and positive coterms are synthesisable. This combi...","url_abs":"https://arxiv.org/abs/2512.07511","url_pdf":"https://arxiv.org/pdf/2512.07511v1","authors":"[\"Zanzi Mihejevs\",\"Jules Hedges\"]","published":"2025-12-08T12:47:25Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.LO\"]","methods":"[]","has_code":false}