Canonical bidirectional typechecking

Zanzi Mihejevs, Jules Hedges

We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised $\mu \tilde{\mu }$-calc…