2025/12/08 by Mihejevs, Zanzi, Hedges, Jules · 1 citation
Computer Science · Mathematics · #Logic, programming, and type systems #Formal Methods in Verification #Homotopy and Cohomology in Algebraic Topology
paper · doi:10.48550/arxiv.2512.07511
We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised μμ-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.