Person. Zanzi Mihejevs

Papers

Canonical bidirectional typechecking mihejevs-2025-canonical

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.
arXiv
zanzimihejevs person entries/rolodex/zanzimihejevs.hel