\gdef\jdg#1{\:\mathrm{#1}} \gdef\decode#1{\mathord{\uparrow}#1} \gdef\code#1{\mathord{\downarrow}#1} \gdef\jty{\:\mathrm{ty}} \gdef\jprop{\:\mathrm{prop}} \gdef\jtrue{\:\mathrm{true}} \gdef\yields{\vdash} \gdef\ms#1{\mathsf{#1}} \gdef\mc#1{\mathcal{#1}} \gdef\Open#1{{\Large \circ}{#1}} \gdef\Close#1{{\Large \bullet}{#1}} \gdef\OpenEta{\eta^{\circ}} \gdef\CloseEta{\eta^{\bullet}} \gdef\isStatic#1{\mathrm{isStatic}(#1)} \gdef\isDynamic#1{\mathrm{isDynamic}(#1)} \gdef\ite#1#2#3{\mathbf{if}\:\:#1\:\:\mathbf{then}\:\:#2\:\:\mathbf{else}\:\:#3} \gdef\StOpn{{\Large \circ}_{\mathrm{st}}} \gdef\Opn{{\Large \circ}} \gdef\op{^\mathrm{op}} \gdef\CC{\mathbb{C}}

An Algebraic Approach to the Static/Dynamic Phase Distinction for Module Calculi

May 07, 2026

Owen Lynch